We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic. while all non-invalidating behavior is retained. This induces maximal permissiveness in the context of supervisory control. Research presented in this paper allows a system model to be constrained according to a broad set of liveness, safety and fairness specifications of desired behavior, and embraces most concepts from Ramadge-Wonham supervisory control, including controllability and marker-state reachability. Synthesis is defined in this paper as a formal construction, which allowed a careful validation of its correctness using the Coq proof assistant.
Ramadge-Wonham supervisory control @cite_4 defines a broadly-embraced meth-odology for controller synthesis on deterministic plant models for requirements specified using automata. It defines a number of key elements in the relationship between plant and controlled system, such as controllability, marker-state reachability, deadlock-freeness and maximal permissiveness. Despite the fact that a strictly separated controller offers advantages from a developmental or implementational point of view, we argue that increased abstraction and flexibility justifies research into control synthesis for non-deterministic models. In addition, we emphasize that the automata-based description of desired behavior in the Ramadge-Wonham framework @cite_4 does not allow the specification of requirements of existential nature. For instance, in this framework it is not possible to specify that a step labeled with a particular event exist, hence the choice of modal logic as our requirement formalism.
@cite_4
1979349468
The paper studies the control of a class of discrete event processes, i.e., processes that are discrete, asynchronous and possibly nondeterministic. The controlled process is described as the generator of a formal language, while the controller, or supervisor, is constructed from a recognizer for a specified target language that incorporates the desired closed-loop system behavior. The existence problem for a supervisor is reduced to finding the largest controllable language contained in a given legal language. Two examples are provided.