A process-theoretic approach to supervisory coordination under partial observation

We propose a synthesis-centric model-based engineering framework for safe and nonblocking coordination of distributed components of complex high-tech systems. The framework is based on a process theory geared towards supervisory coordination and control of nondeterministic discrete-event systems under partial observation. Supervisory control theory deals with automated synthesis of provably correct models of supervisory controllers based on formal models of the system components and a formalization of the coordination requirements. Based on the obtained models, code generation can be used to implement the supervisory controllers in software, on a PLC, or an embedded (micro)processor. The proposed theory employs communication actions to distinguish between the different flows of information, i.e., observation of the system behavior and supervision by means of forwarding control signals. In addition, we consider the case of partial observation, where some behavior of the unsupervised system is hidden from the supervisory controller, e.g., due to lack of sensory information or internal inter-component communication. We revisit the notion of partial observation and treat it as a property of the supervisor, instead of conditioning the control requirements, which is a standard approach. By employing a behavior relation termed partial bisimulation, we are able to succinctly and transparently capture the notions of controllability and partial observability.