Maximal synthesis for Hennessy-Milner logic

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

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

This article concerns the maximal synthesis for Hennessy-Milner Logic on Kripke structures with labeled transitions. We formally define, and prove the validity of, a theoretical framework that modifies a Kripke model to the least possible extent in order to satisfy a given HML formula. Applications of this work can be found in the field of controller synthesis and supervisory control for discrete-event systems. Synthesis is realized technically by first projecting the given Kripke model onto a bisimulation-equivalent partial tree representation, thereby unfolding up to the depth of the synthesized formula. Operational rules then define the required adaptations upon this structure in order to achieve validity of the synthesized formula. Synthesis might result in multiple valid adaptations, which are all related to the original model via simulation. Each simulant of the original Kripke model, which satisfies the synthesized formula, is also related to one of the synthesis results via simulation. This indicates maximality, or maximal permissiveness, in the context of supervisory control. In addition to the formal construction of synthesis as presented in this article, we present it in algorithmic form and analyze its computational complexity. Computer-verified proofs for two important theorems in this article have been created using the Coq proof assistant.
Original languageEnglish
Pages (from-to)1-21
JournalACM Transactions on Embedded Computing Systems
Volume14
Issue number1
DOIs
Publication statusPublished - 2015

Fingerprint

Discrete event simulation
Computational complexity
Controllers

Cite this

van Hulst, A. ; Reniers, M.A. ; Fokkink, W.J. / Maximal synthesis for Hennessy-Milner logic. In: ACM Transactions on Embedded Computing Systems. 2015 ; Vol. 14, No. 1. pp. 1-21.
@article{cfbb00ce595b4a40a88822ab795a7f82,
title = "Maximal synthesis for Hennessy-Milner logic",
abstract = "This article concerns the maximal synthesis for Hennessy-Milner Logic on Kripke structures with labeled transitions. We formally define, and prove the validity of, a theoretical framework that modifies a Kripke model to the least possible extent in order to satisfy a given HML formula. Applications of this work can be found in the field of controller synthesis and supervisory control for discrete-event systems. Synthesis is realized technically by first projecting the given Kripke model onto a bisimulation-equivalent partial tree representation, thereby unfolding up to the depth of the synthesized formula. Operational rules then define the required adaptations upon this structure in order to achieve validity of the synthesized formula. Synthesis might result in multiple valid adaptations, which are all related to the original model via simulation. Each simulant of the original Kripke model, which satisfies the synthesized formula, is also related to one of the synthesis results via simulation. This indicates maximality, or maximal permissiveness, in the context of supervisory control. In addition to the formal construction of synthesis as presented in this article, we present it in algorithmic form and analyze its computational complexity. Computer-verified proofs for two important theorems in this article have been created using the Coq proof assistant.",
author = "{van Hulst}, A. and M.A. Reniers and W.J. Fokkink",
year = "2015",
doi = "10.1145/2680540",
language = "English",
volume = "14",
pages = "1--21",
journal = "ACM Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery (ACM)",
number = "1",

}

Maximal synthesis for Hennessy-Milner logic. / van Hulst, A.; Reniers, M.A.; Fokkink, W.J.

In: ACM Transactions on Embedded Computing Systems, Vol. 14, No. 1, 2015, p. 1-21.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Maximal synthesis for Hennessy-Milner logic

AU - van Hulst, A.

AU - Reniers, M.A.

AU - Fokkink, W.J.

PY - 2015

Y1 - 2015

N2 - This article concerns the maximal synthesis for Hennessy-Milner Logic on Kripke structures with labeled transitions. We formally define, and prove the validity of, a theoretical framework that modifies a Kripke model to the least possible extent in order to satisfy a given HML formula. Applications of this work can be found in the field of controller synthesis and supervisory control for discrete-event systems. Synthesis is realized technically by first projecting the given Kripke model onto a bisimulation-equivalent partial tree representation, thereby unfolding up to the depth of the synthesized formula. Operational rules then define the required adaptations upon this structure in order to achieve validity of the synthesized formula. Synthesis might result in multiple valid adaptations, which are all related to the original model via simulation. Each simulant of the original Kripke model, which satisfies the synthesized formula, is also related to one of the synthesis results via simulation. This indicates maximality, or maximal permissiveness, in the context of supervisory control. In addition to the formal construction of synthesis as presented in this article, we present it in algorithmic form and analyze its computational complexity. Computer-verified proofs for two important theorems in this article have been created using the Coq proof assistant.

AB - This article concerns the maximal synthesis for Hennessy-Milner Logic on Kripke structures with labeled transitions. We formally define, and prove the validity of, a theoretical framework that modifies a Kripke model to the least possible extent in order to satisfy a given HML formula. Applications of this work can be found in the field of controller synthesis and supervisory control for discrete-event systems. Synthesis is realized technically by first projecting the given Kripke model onto a bisimulation-equivalent partial tree representation, thereby unfolding up to the depth of the synthesized formula. Operational rules then define the required adaptations upon this structure in order to achieve validity of the synthesized formula. Synthesis might result in multiple valid adaptations, which are all related to the original model via simulation. Each simulant of the original Kripke model, which satisfies the synthesized formula, is also related to one of the synthesis results via simulation. This indicates maximality, or maximal permissiveness, in the context of supervisory control. In addition to the formal construction of synthesis as presented in this article, we present it in algorithmic form and analyze its computational complexity. Computer-verified proofs for two important theorems in this article have been created using the Coq proof assistant.

U2 - 10.1145/2680540

DO - 10.1145/2680540

M3 - Article

VL - 14

SP - 1

EP - 21

JO - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 1

ER -