Finite Response and Confluence of State-based Supervisory Controllers

The development of logic controllers for cyber-physical systems is a difficult and error-prone process. Supervisor synthesis can ease the development process, by synthesizing a correct-by-construction supervisor from a model of the plant and a model of the control requirements. Subsequently, this synthesized supervisor can be used to automatically generate the controller code. However, for a supervisor to be implemented as a (logic) controller, additional properties need to be satisfied which are not guaranteed by supervisor synthesis. These properties are finite response and confluence. In the literature, conditions are provided for a supervisor, modeled as a set of finite-state automata, to have finite response and to be confluent. Algorithms are defined to check these conditions. Recently, extended finite-state automata, i.e, automata augmented with variables, are being used increasingly often in the context of supervisory control. In this paper, sufficient conditions and algorithms are provided that can be used to verify if a supervisor, modeled as a set of extended finite-state automata, has finite response and is confluent. The algorithms are applied to three case studies from the literature to demonstrate their applicability to models used for supervisor synthesis.