Algebraic Approach to Synthesis of State-Based Opacity

Our previous works have discussed the state-based opacity validation of finite state machines from an algebraic approach, what should we do if finite state machines are verified to be non-opaque? In this paper, the state-based opacity synthesis problems of finite state machines are investigated by using a novel algebraic method. According to the algebraic representation, which has been established for the dynamics of finite state machine in our previous work, two perspectives from the opacity synthesis are investigated including feedback supervisory control and feedforward observation edition. For the feedback supervisory controller, the closed-loop system can be driven to satisfy the opacity condition by disabling the controllable events. For the observation editor, the opacity can also be guaranteed just by assigning some specific events in the observable event set. By introducing the semi-tensor product of matrices, both synthesis problems can be solved by constructing some algebraic equation system. Finally, a typical example is given to demonstrate the proposed method.