Maximally permissive controlled system synthesis for non-determinism and modal logic

A. C. van Hulst*, M.A. Reniers, W. J. Fokkink

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from Gödel-Löb logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.

Original languageEnglish
Pages (from-to)109-142
Number of pages34
JournalDiscrete Event Dynamic Systems
Issue number1
Publication statusPublished - 1 Mar 2017


  • Controllability
  • Controlled system synthesis
  • Maximal permissiveness
  • Modal logic
  • Non-determinism
  • Partial bisimulation


Dive into the research topics of 'Maximally permissive controlled system synthesis for non-determinism and modal logic'. Together they form a unique fingerprint.

Cite this