Supervisor Fortification Against Covert Actuator Attacks

This work considers the supervisor fortification problem against covert actuator attacks. A supervisor S '' is said to fortify the supervisor S, the latter of which is non-resilient against covert actuator attacks, if S ' satisfies two conditions: 1) any covert actuator attack cannot cause damage infliction against S ', and 2) S ' is control equivalent to S. The key result of this work is that we show the problem of determining the existence of a fortified supervisor to defend against any covert actuator attack, an '' exist-for all '' decidability question, is decidable. To show the decidability result, we provide a complete and sound procedure that ensures to synthesize a fortified supervisor as long as there exists one.