### Abstract

Original language | English |
---|---|

Pages (from-to) | 1-21 |

Journal | ACM Transactions on Embedded Computing Systems |

Volume | 14 |

Issue number | 1 |

DOIs | |

Publication status | Published - 2015 |

### Fingerprint

### Cite this

*ACM Transactions on Embedded Computing Systems*,

*14*(1), 1-21. https://doi.org/10.1145/2680540

}

*ACM Transactions on Embedded Computing Systems*, vol. 14, no. 1, pp. 1-21. https://doi.org/10.1145/2680540

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

Research output: Contribution to Journal › Article › Academic › peer-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 -