Opacity Enforcement in Discrete Event Systems Using Extended Insertion Functions Under Inserted Language Constraints

Opacity is a confidentiality property capturing the fact that certain secret behavior of a system cannot be revealed under any system evolution. Current-state opacity can be enforced by using an extended insertion mechanism, which is capable of inserting fake symbols before and after an actual output, in real time as the system evolves. This article studies the enforcement of current-state opacity for systems modeled by finite state automata using an extended insertion strategy under constraints on the way symbols can be inserted before and after an actual symbol generated by the system (e.g., constraints on the type, order, and number of inserted symbols). More specifically, we consider inserted language constraints captured by the notion of (L-b, L-a)-enforceability, where L-b is the set of strings that can be inserted before, and L-a is the set of strings that can be inserted after an observed event. If L-b and L-a are regular languages, a verifier is constructed to derive a necessary and sufficient condition for opacity enforceability, and also to formulate an extended insertion strategy (if viable).