Return
Opacity Enforcement in Discrete Event Systems Using Modification Functions
DOI:10.1109/TASE.2024.3391617.png)
Abstract
En 中文
Opacity of a discrete event system is a confidentiality property that characterizes instances when the secret behavior of the system cannot be revealed. This paper considers current-state opacity with respect to a set of secret states, and addresses the opacity enforcement problem via modification functions that are capable of replacing in real-time the output of the underlying system with another output, aiming to prevent the intruder from inferring the secret. We study modification functions that are constrained, i.e., they may not be able to modify certain outputs or they may have restrictions in how they modify a particular output. A system is said to be emc-enforceable if opacity can be enforced via modification functions under the given event modification constraints (emc). To verify whether a system is emc-enforceable, we construct a verifier, based on which a necessary and sufficient condition is obtained. If a system is emc-enforceable, an algorithm is developed to compute a modification strategy based on the verifier to enforce opacity. For m-enforceability, a special case of emc-enforceability without constraints, two necessary and sufficient conditions to verify and enforce opacity with reduced complexity are presented, one based on a system estimator and the other based on a detector.
Keywords:
Sensors
Robot sensing systems
Symbols
Observers
Discrete-event systems
Automata
Cyber-physical systems
Discrete event system
finite state automaton
opacity
modification function
event modification constraint
Journal
IF:
6.4
Papers:
4.9K
Citations:
1.6W

