{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:24Z","timestamp":1750308564789,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,21]],"date-time":"2015-01-21T00:00:00Z","timestamp":1421798400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EU FP7 Programme","award":["295261 (MEALS)"],"award-info":[{"award-number":["295261 (MEALS)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,1,21]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/2680540","type":"journal-article","created":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T14:05:51Z","timestamp":1422453951000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Maximal Synthesis for Hennessy-Milner Logic"],"prefix":"10.1145","volume":"14","author":[{"given":"A. C. Van","family":"Hulst","sequence":"first","affiliation":[{"name":"Eindhoven University of Technology, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. A.","family":"Reniers","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W. J.","family":"Fokkink","sequence":"additional","affiliation":[{"name":"VU University Amsterdam, Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,1,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.07.001"},{"key":"e_1_2_1_3_1","unstructured":"M. Antoniotti and B. Mishra. 1995. The Supervisor Synthesis Problem for Unrestricted CTL Is NP-complete. Technical Report. New York University. M. Antoniotti and B. Mishra. 1995. The Supervisor Synthesis Problem for Unrestricted CTL Is NP-complete. Technical Report. New York University."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"J. Baeten B. van Beek A. van Hulst and J. Markovski. 2011. A process algebra for supervisory coordination. In Process Algebra and Coordination. EPTCS 36--55. J. Baeten B. van Beek A. van Hulst and J. Markovski. 2011. A process algebra for supervisory coordination. In Process Algebra and Coordination. EPTCS 36--55.","DOI":"10.4204\/EPTCS.60.3"},{"key":"e_1_2_1_5_1","unstructured":"B. Barras S. Boutin C. Cornes J. Courant J. Filliatre E. Gimenez H. Herbelin G. Huet C. Munoz and C. Murthy. 1997. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report. INRIA. B. Barras S. Boutin C. Cornes J. Courant J. Filliatre E. Gimenez H. Herbelin G. Huet C. Munoz and C. Murthy. 1997. The Coq Proof Assistant Reference Manual: Version 6.1. Technical Report. INRIA."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"R. Bull and K. Segerberg. 1994. Basic modal logic. In Handbook of Philosophical Logic. Springer 1--88. R. Bull and K. Segerberg. 1994. Basic modal logic. In Handbook of Philosophical Logic. Springer 1--88.","DOI":"10.1007\/978-94-009-6259-0_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"C. Cassandras and S. Lafortune. 1999. Introduction to Discrete Event Systems. Springer. C. Cassandras and S. Lafortune. 1999. Introduction to Discrete Event Systems. Springer.","DOI":"10.1007\/978-1-4757-4070-7"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383878"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"A. Deshpande and P. Varaiya. 1996. Semantic tableau for control of PLTL formulae. In Decision and Control. IEEE 2243--2248. A. Deshpande and P. Varaiya. 1996. Semantic tableau for control of PLTL formulae. In Decision and Control. IEEE 2243--2248.","DOI":"10.1109\/CDC.1996.572984"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882305"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430543"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0363012902409982"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Vardi. 2000. &mu;-calculus synthesis. In Mathematical Foundations of Computer Science. Springer 497--507. O. Kupferman and M. Vardi. 2000. &mu;-calculus synthesis. In Mathematical Foundations of Computer Science. Springer 497--507.","DOI":"10.1007\/3-540-44612-5_45"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2893"},{"key":"e_1_2_1_17_1","first-page":"5","article-title":"Synthesis from component libraries","volume":"15","author":"Lustig Y.","year":"2013","journal-title":"Software Tools for Technology Transfer"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.015"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357237"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"O. Sokolsky and S. Smolka. 1994. Incremental model checking in the modal mu-calculus. In Computer Aided Verification. Springer 351--363. O. Sokolsky and S. Smolka. 1994. Incremental model checking in the modal mu-calculus. In Computer Aided Verification. Springer 351--363.","DOI":"10.1007\/3-540-58179-0_67"},{"volume-title":"Concurrency Theory","author":"van Glabbeek R.","key":"e_1_2_1_23_1"},{"volume-title":"Coq v8.3 Formalization.","year":"2013","author":"van Hulst A.","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.4"},{"volume-title":"Workshop on Discrete Event Systems. IEEE, 278--285","author":"van Hulst A.","key":"e_1_2_1_26_1"},{"volume-title":"41st International Conference on Current Trends in Theory and Practice of Computer Science. Springer, 230--240","author":"van Hulst A.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/239519.239527"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1067915.1067920"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2680540","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2680540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:15Z","timestamp":1750273455000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2680540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,21]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1,21]]}},"alternative-id":["10.1145\/2680540"],"URL":"https:\/\/doi.org\/10.1145\/2680540","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,1,21]]},"assertion":[{"value":"2013-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}