Opacity of Parametric Discrete Event Systems: Models, Decidability, and Algorithms

TL;DR

This paper explores the opacity analysis of parametric discrete event systems modeled by extended finite automata, establishing decidability results and algorithms for simplified models, and highlighting the complexity and expressiveness differences.

Contribution

It introduces and compares EFAs and EP-EFAs models, proves undecidability for EFAs, and develops verification algorithms for opacity properties in EP-EFAs.

Findings

EFAs are more expressive than EP-EFAs.

Opacity for EFAs is generally undecidable.

Verification algorithms for EP-EFAs are proposed with complexity analysis.

Abstract

Finite automata (FAs) model is a popular tool to characterize discrete event systems (DESs) due to its succinctness. However, for some complex systems, it is difficult to describe the necessary details by means of FAs model. In this paper, we consider a kind of extended finite automata (EFAs) in which each transition carries a predicate over state and event parameters. We also consider a type of simplified EFAs, called Event-Parameters EFAs (EP-EFAs), where the state parameters are removed. Based upon these two parametric models, we investigate the problem of opacity analysis for parametric DESs. First of all, it is shown that EFAs model is more expressive than EP-EFAs model. Secondly, it is proved that the opacity properties for EFAs are undecidable in general. Moreover, the decidable opacity properties for EP-EFAs are investigated. We present the verification algorithms for current-state opacity, initial-state opacity and infinite-step opacity, and then discuss the complexity. This paper establishes a preliminary theory for the opacity of parametric DESs, which lays a foundation for the opacity analysis of complex systems.