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.
|Title of host publication||Proceedings - 2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013|
|Number of pages||10|
|Publication status||Published - 21 Oct 2013|
|Event||2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013 - Barcelona, Spain|
Duration: 8 Jul 2013 → 10 Jul 2013
|Conference||2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013|
|Period||8/07/13 → 10/07/13|