Shaopeng Hu, Yihui Hu, Jan Komenda, Zhiwu Li
In this paper, we formalize and solve the problems of active diagnosis for discrete event systems modeled with labeled Petri nets that may enter deadlocks under coordinated sensor and actuator attacks. Given a plant, a sensor attacker has the ability to edit certain sensor readings to conceal the faults to confuse the operator. An actuator attacker may exist in the control channel between a plant and its supervisor, and has the ability to tamper with the control actions commanded by the supervisor such that the plant remains nondiagnosable under the control of the supervisor. Furthermore, sensor and actuator attackers collaborate to attack a plant and maintain furtivity, i.e., their presence should not be discovered by the operator. In order to test the diagnosability under such attacks, a structure, called an extended verifier, is established. It is shown that a labeled Petri net that may enter deadlocks under coordinated sensor and actuator attacks is diagnosable if and only if the verifier does not contain the confused cycles composed exclusively of pairs of faulty states and normal states. This result also provides necessary and sufficient conditions for active diagnosis under coordinated sensor and actuator attacks by designing a maximally resilient supervisor. Examples are presented to demonstrate the proposed method.