Verifying performance of supervised plants

Supervisory control theory deals with synthesis of models of supervisory controllers that ensure safe and nonblocking behavior, based on discrete-event models of the uncontrolled system and the control requirements. Extensions, like optimal supervision, additionally ascertain that given performance requirements are met by the controller as well. Unfortunately, ensuring optimality during supervisor synthesis proved to be computationally challenging. Therefore, we propose to separate supervisor synthesis and ensuring performance. To handle the stochastic behavior efficiently, we treat the Markovian delays syntactically and we employ existing synthesis tools for non-stochastic plants. To this end, we develop a process theory that can specify control loops of nondeterministic stochastic systems with state-based observations. After obtaining the model of the supervised system, we verify that the supervised system adheres to the given performance requirements by deriving the underlying Markov process and feeding it to a stochastic model checker. We illustrate the approach by estimating performance and reliability measures for the printing process of a high-tech Oce´ printer.