Towards Optimal Supervisory Control of Discrete-Time Stochastic Discrete-Event Processes with Data

We propose a model-based systems engineering framework for supervisory control and probabilistic model checking of discrete-time stochastic discrete-event systems. Supervisory control theory deals with synthesis of models of supervisory controllers that ensure safe and nonblocking behavior, based on models of the uncontrolled system and the control requirements. However, guaranteeing only safety and nonblocking properties of the supervised system is not sufficient, and often performance measures must be taken into account. Unfortunately, treating optimality in the synthesis procedure is a costly undertaking. Therefore, we propose to decouple the synthesis of the supervisor that caters for functional aspects of the system from the performance evaluation that considers the quantitative aspects. We provide an appropriate abstraction of the stochastic behavior, which enables us to employ standard supervisory controller synthesis tools. The synthesized supervisor is, thereafter, coupled with the stochastic model of the unsupervised system, and abstracted to a discretetime Markov process, which is fed to a probabilistic model checker to validate the performance requirements.