Maximal synthesis for Hennessy-Milner logic

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

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

We present a solution for the synthesis on Kripke structures with labelled transitions, with respect to Hennessy-Milner Logic. This encompasses the definition of a theoretical framework that is able to express how such a transition system should be modified in order to satisfy a given HMLformula. The transition system is mapped under bisimulation equivalence onto a recursive structure, thereby unfolding up to the applicable reach of a given HML-formula. Operational rules define the required adaptations to ensure validity upon this structure. Synthesis might result in multiple valid adaptations which are all related to the original transition system via simulation. The set of synthesized products contains an outcome which is maximal with respect to all deterministic simulants which satisfy the HML-formula.

Original languageEnglish
Title of host publicationProceedings - 2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013
Pages1-10
Number of pages10
DOIs
Publication statusPublished - 21 Oct 2013
Event2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013 - Barcelona, Spain
Duration: 8 Jul 201310 Jul 2013

Conference

Conference2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013
CountrySpain
CityBarcelona
Period8/07/1310/07/13

Cite this