Process-Theoretic Models for Optimal and Reliable Supervision

In this proposal we aim to advance optimal supervisory control synthesis by employing a new process-theoretic approach to nondeterministic Markovian discrete-event systems. Supervisory control theory deals with automated synthesis of controllers based on models of the uncontrolled system and control requirements. Optimal supervision ensures in addition that given performance measures and reliability requirements are met. It is known that even without stochastic behavior, supervisory control of nondeterministic systems is a tricky problem. For that purpose, we employ a process-theoretic approach to supervisory control that is sufficiently powerful to deal with nondeterminism by employing behavior relations that capture the relationship between the controller and the system. In this proposal, we advance the theory by turning to stochastic extensions of standard process-theoretic models, conveniently providing qualitative and quantitative modeling capabilities. As primary candidates we consider Interactive Markov chains and their derivatives, which represent orthogonal extensions of labeled transition systems with stochastic delays. Moreover, they subsume standard models for supervisor synthesis and performance analysis, extending them with unrestricted nondeterminism. We aim to develop theory, algorithms, and tools for supervisor synthesis and minimization for these Markovian models, while preserving the constitutional performance measures and controllability properties. To ensure that performance and reliability measures are met, we will employ stochastic model-checking techniques. The supervised behavior under such control satis?es extended liveness properties, ensuring desired functionalities and reliability of the controlled system, while meeting given performance speci?cations that guarantee its efficiency. We will employ the framework to reiterate on old and carry out new industrial studies.