Maximal synthesis for Hennessy-Milner logic with the box modality

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

    Research output: Contribution to journalConference articlepeer-review

    2 Citations (Scopus)


    This paper presents a novel approach to adapt a behavioral model in order to satisfy a requirement in Hennessy-Milner Logic, including an additional box modality operator, expressing an invariant formula. Control system synthesis, as defined in this way, retains all non-invalidating behavior, and thereby guarantees maximal permissiveness for supervisory control. This research extends earlier work by embracing a broader synthesized logic, enabling synthesis with respect to invariant formulas for non-deterministic behavioral models. All definitions and proofs in this paper have been computer verified using the Coq proof assistant.
    Original languageEnglish
    Pages (from-to)278-285
    Number of pages8
    JournalIFAC Proceedings Volumes
    Issue number2
    Publication statusPublished - 2014
    Event12th International Workshop on Discrete Event Systems (WODES 2014) - Cachan, France
    Duration: 14 May 201416 May 2014
    Conference number: 12


    • Control system synthesis
    • Invariants
    • Supervisory control
    • Temporal logic


    Dive into the research topics of 'Maximal synthesis for Hennessy-Milner logic with the box modality'. Together they form a unique fingerprint.

    Cite this