User Tools

Site Tools


ProThOS - Process-Theoretic Models for Supervisory Control

Project duration: 15.08.2011 – 14.08.2014

NWO grant no. 600.065.120.11N124



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 satisfies extended liveness properties, ensuring desired functionalities and reliability of the controlled system, while meeting given performance specifications that guarantee its efficiency. We will employ the framework to reiterate on old and carry out new industrial studies.



  • J. Markovski, J.M. van de Mortel-Fronczak: “Modeling for Safety in a Synthesis-Centric Systems Engineering Framework”, In The proceedings of SASSUR 2012, LNCS 7613, pp. 36-51
  • J. Markovski: “Communicating Processes with Data for Supervisory Coordination”, In the proceedings of FOCLASA 2012, EPTCS 91, pp. 97-111
  • J. Markovski, M. A. Reniers: “Verifying Liveness in Supervised Systems Using UPPAAL and mCRL2”, accepted at ICTI 2012, LNCS, 2012
  • J. Markovski, E.S. Estens Musa, M. A. Reniers: “Extending a Synthesis-Centric Model-Based Systems Engineering Framework with Stochastic Model Checking”, accepted at PASM 2012, ENTCS, 2012
  • J. Markovski: “Coarsest Controllability-Preserving Plant Minimization”, accepted at WODES 2012
  • J. Markovski: “Performance Evaluation with Cost Estimation for Supervised Systems”, accepted at SMC 2012
  • J. Markovski, M.A. Reniers: “An Integrated State- and Event-Based Framework for Verifying Liveness in Supervised Systems”, accepted at ICARCV 2012
  • J. Markovski: “A Synthesis-Based Framework for Systems Engineering”, short paper at SYNT 2012
  • J. Markovski: “Process Theory for Supervisory Control with Partial Observation of Events and States”, accepted CDC 2012
  • J. Markovski: “Scalable Minimization Algorithm for Partial Bisimulation”, in the Proceedings of FMDS 2012, EPTCS 86, pp. 9-16
  • J. Markovski: “Process Theory for Supervisory Control of Stochastic Systems with Data”, accepted at ETFA 2012
  • J. Markovski: “A Process-Theoretic State-Based Framework for Live Supervision”, in the Proceedings of CASE 2012, IEEE, pp. 676 - 681
  • J. Markovski, P.R. D'Argenio, J.C.M. Baeten, and E.P. de Vink: “Reconciling Real and Stochastic Time: the Need for Probabilistic Refinement”, Formal Aspects of Computing, vol. 24(4-6), Springer, 2012, pp.497-518
  • J. Markovski, M.A. Reniers: “Verifying Performance of Supervised Plants”, in the Proceedings of ACSD 2012, IEEE, pp. 52-61
  • J. Markovski, D.A. van Beek, and J.C.M. Baeten: “Partially-Supervised Plants: Embedding Control Requirements in Plant Components”, in the proceedings of iFM 2012, LNCS, vol. 7321, Springer, pp. 253-267
  • J. Markovski: “Towards Supervisory Control for Interactive Markov Chains: Plant Minimization”, in the Proceedings of ICCA 2011, IEEE, pp. 1195 - 1200
  • J. Markovski: “Towards Supervisory Control of Interactive Markov Chains: Controllability”, in the Proceedings of ACSD 2011, pp. 108 – 117, IEEE, 2011

Developed Tools:

  • Supremica2UPPAAL - Java application that translates a Supremica model of a supervised plant to a UPPAAL automaton for the purpose of state-based verification
  • Supremica2mCRL2- Java application that transforms a Supremica supervised plant to an mCRL2 labeled transition system
  • Supremica2{IMC, MRMC} - Java applications that extract an MRMC performance model from an integrated Supremica model of a supervised plant
  • MRMCCosts - Java application that enables convenient specification of a cost model based on state labels and translates it as an input for MRMC

Download link

prothos/start.txt · Last modified: Monday, 15 October 2012 : 02:26:08 by jmarkovs