Supervisory control of discrete-event systems under external attacks.

• This paper involves the supervisor design for a discrete event system under attacks in the framework of labeled Petri nets. • The reachability graph of a labeled Petri net is compactly represented by an observer. • A novel structure, namely a product observation reachability graph constructed from a plant and its specification, is proposed to decide the existence of a supervisor. Resilience is a critical criterion to evaluate a networked system including discrete-event systems (DESs). This research touches upon the supervisory control problem of a DES modeled with labeled Petri nets under malicious attacks. Attacks on a system can be categorized into actuator attacks and sensor attacks. The former may cause a failure of an actuator for executing the commands issued from a supervisor that enforces a specification. The latter may corrupt an observation (i.e., a sequence of observable transition labels) from a sensor by different types of attacks such as insertion, removal, and replacement of transition labels. For actuator attacks, if we can detect them and disable some particular controllable transition labels before reaching a state that does not satisfy the specification, then we can find a modified supervisor to enforce the specification. For sensor attacks, we assume that, once a time, only one attack can be carried out, i.e., the attacker does not change the attack during an observation corruption. Given a specification, we consider in a plant model any two feasible transition sequences that share the same corrupted observation under attacks. It is shown that there exists a supervisor to enforce the specification if the one-step controllable extensions of the two transition sequences either satisfy or violate the specification simultaneously. To this end, a novel structure, namely a product observation reachability graph constructed from a plant and its specification, is proposed to decide the existence of such a supervisor by checking whether each state in the graph satisfies a particular condition. The application of the reported methods is demonstrated through examples. [ABSTRACT FROM AUTHOR]