On Decidability of Existence of Fortified Supervisors Against Covert Actuator Attackers

This work investigates the existence of fortified supervisors against covert actuator attackers. For a supervisor $S$ that is nonresilient against covert actuator attackers, a fortified supervisor $S<^>{\prime }$ satisfies two requirements: 1) $S<^>{\prime }$ is resilient against any covert actuator attacker, and 2) the original closed-behavior of the closed-loop system under $S$ is preserved. We design a sound and complete procedure to show the problem of determining the existence of a fortified supervisor against covert actuator attackers is decidable. The decidability result is also extended to the case against the worst-case attacker.