Process theory for supervisory control of stochastic systems with data

We propose a process theory for supervisory control of stochastic nondeterministic plants with data-based observations. The Markovian process theory with data relies on the notion of Markovian partial bisimulation to capture controllability of stochastic nondeterministic systems. It presents a theoretical basis for a model-based systems engineering framework that is based on state-of-the-art tools: we employ Supremica for supervisor synthesis and MRMC for stochastic model checking and performance evaluation. We present the process theory and discuss the implementation of the framework.