Towards optimal supervisory controller synthesis of stochastic nondeterministic discrete-event systems

We synthesize supervisory controllers for discrete-time stochastic discrete-event systems with unrestricted nondeterminism by employing data-based control requirements and by abstracting from the stochastic aspects of the original system. This approach enables the use of standard synthesis tools, like Supremica, whereas the probabilistic behavior of the supervised system can be analyzed by using probabilistic model checking, e.g., by employing PRISM. We develop a process theory that provides for the appropriate abstractions of the probabilistic timed behavior of the original system and for compositional model transformation from Supremica to PRISM. We illustrate the proposed framework on a case study dealing with movement coordination of automated guided vehicles in pipeless plants.