On Decidability of Existence of Fortified Supervisors Against Covert Actuator Attackers

TL;DR

This paper addresses the problem of synthesizing fortified supervisors that are resilient against covert actuator attackers while preserving the original system behavior, establishing the problem's decidability through a sound and complete procedure.

Contribution

It introduces a decidable method for synthesizing fortified supervisors resilient to covert actuator attackers, extending to worst-case attacker scenarios.

Findings

Decidability of fortified supervisor existence established

Sound and complete synthesis procedure developed

Extension to worst-case attacker scenarios discussed

Abstract

This work investigates the problem of synthesizing fortified supervisors against covert actuator attackers. For a non-resilient supervisor S, i.e., there exists at least a covert actuator attacker that is capable of inflicting damage w.r.t S, a fortified supervisor S' satisfies two requirements: 1) S' is resilient against any covert actuator attacker, and 2) the original closed-behavior of the closed-loop system under S is preserved, that is, S' is control equivalent to S. By designing a sound and complete procedure, we show the problem of determining the existence of a fortified supervisor against covert actuator attackers is decidable. We also discuss how to extend the decidability result to the case against the worst-case attacker.