Opacity formulations and verification in discrete event systems
AuthorHadjicostis, Christoforos N.
PublisherInstitute of Electrical and Electronics Engineers Inc.
Source19th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2014
19th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2014
Google Scholar check
MetadataShow full item record
In many emerging security applications, a property of a system, that may reveal important details about its behaviour, needs to be kept secret (opaque) to outside observers (intruders). Motivated by such applications, several authors have formalized, analyzed, and described methods to verify notions of opacity in discrete event systems of interest. This paper offers a review of various definitions of opacity, along with methodologies for their verification and complexity analysis. We review state-based notions of opacity (namely, current-state opacity and initial-state opacity) in non-deterministic finite automata, as well as their extensions to stochastic settings. Specifically, we discuss these notions of opacity and methods to verify them in discrete event systems modeled by non-deterministic finite automata (NFA's) or probabilistic finite automata (PFA's). © 2014 IEEE.