{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:03:50Z","timestamp":1761487430209,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2005,5]]},"abstract":"<jats:p>Model checking and supervisor synthesis have been successful in solving different design problems related to discrete systems in the last decades. In this paper, we analyze some advantages and drawbacks of these approaches and combine them for mutual improvement. We achieve this through a generalization of the supervisory control problem proposed by Ramadge and Wonham. The objective of that problem is to synthesize a supervisor which constrains a system's behavior according to a given specification, ensuring controllability and coaccessibility. By introducing a new representation of the solution using systems of \u03bc-calculus equations, we are able to handle these two conditions separately and thus to exchange the coaccessibility requirement by any condition that could be used in model checking. Well-known results on \u03bc-calculus model checking allow us to easily assess the computational complexity of any generalization. Moreover, the model checking approach also delivers algorithms to solve the generalized synthesis problem. We include an example in which the coaccessibility requirement is replaced by fairness constraints. The paper also contains an analysis of related work by several authors.<\/jats:p>","DOI":"10.1145\/1067915.1067920","type":"journal-article","created":{"date-parts":[[2005,8,2]],"date-time":"2005-08-02T08:38:10Z","timestamp":1122971890000},"page":"331-362","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Combining supervisor synthesis and model checking"],"prefix":"10.1145","volume":"4","author":[{"given":"Roberto","family":"Ziller","sequence":"first","affiliation":[{"name":"University of Karlsruhe, Karlsruhe, Germany"}]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2005,5]]},"reference":[{"volume-title":"Workshop on Discrete Event Systems","author":"Antoniotti M.","unstructured":"Antoniotti , M. and Mishra , B . 1996. NP-completeness of the supervisor synthesis problem for unrestricted CTL specifications . In Workshop on Discrete Event Systems . Edinburgh, Scotland, UK. Antoniotti, M. and Mishra, B. 1996. NP-completeness of the supervisor synthesis problem for unrestricted CTL specifications. In Workshop on Discrete Event Systems. Edinburgh, Scotland, UK.","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1016\/0020-0190(88)90029-4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1016\/S0304-3975(02)00442-5"},{"key":"e_1_2_1_4_1","volume-title":"Hybrid Systems II","volume":"999","author":"Asarin E.","unstructured":"Asarin , E. , Maler , O. , and Pnueli , A . 1995. Symbolic controller synthesis for discrete and timed systems . In Hybrid Systems II , vol. 999 . LNCS, Springer, Berlin. Asarin, E., Maler, O., and Pnueli, A. 1995. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems II, vol. 999. LNCS, Springer, Berlin."},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1016\/S0304-3975(96)00228-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_7_1","volume-title":"Congress on Information Processing, 308--312","author":"Burstall R.","year":"1974","unstructured":"Burstall , R. 1974 . Program proving considered as hand simulation plus induction . In Congress on Information Processing, 308--312 . Burstall, R. 1974. Program proving considered as hand simulation plus induction. In Congress on Information Processing, 308--312."},{"doi-asserted-by":"crossref","unstructured":"Cassandras C. G. and Lafortune S. 1999. Introduction to Discrete Event Systems. Kluwer Academic Publishers Boston MA.   Cassandras C. G. and Lafortune S. 1999. Introduction to Discrete Event Systems. Kluwer Academic Publishers Boston MA.","key":"e_1_2_1_8_1","DOI":"10.1007\/978-1-4757-4070-7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/5397.5399"},{"doi-asserted-by":"crossref","unstructured":"Clarke E. Grumberg O. and Long D. 1993. Verification tools for finite state concurrent systems. In A Decade of Concurrency---Reflections and Perspectives J. de Bakker W.-P. de Roever and G. Rozenberg Eds. Vol. 803. Springer-Verlag Noordwijkerhout Netherlands 124--175.   Clarke E. Grumberg O. and Long D. 1993. Verification tools for finite state concurrent systems. In A Decade of Concurrency---Reflections and Perspectives J. de Bakker W.-P. de Roever and G. Rozenberg Eds. Vol. 803. Springer-Verlag Noordwijkerhout Netherlands 124--175.","key":"e_1_2_1_10_1","DOI":"10.1007\/3-540-58043-3_19"},{"unstructured":"Clarke Jr E. M. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press London.   Clarke Jr E. M. Grumberg O. and Peled D. A. 1999. Model Checking. The MIT Press London.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","volume-title":"Eds. LNCS","volume":"663","author":"Cleaveland R.","unstructured":"Cleaveland , R. , Klein , M. , and Steffen , B . 1992. Faster model checking for the modal &mu;-calculus. In Computer Aided Verification (CAV'92), G. Bochmann and D. Probst , Eds. LNCS , Vol. 663 . Springer-Verlag, Heidelberg, Germany, 410--422. Cleaveland, R., Klein, M., and Steffen, B. 1992. Faster model checking for the modal &mu;-calculus. In Computer Aided Verification (CAV'92), G. Bochmann and D. Probst, Eds. LNCS, Vol. 663. Springer-Verlag, Heidelberg, Germany, 410--422."},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1016\/0304-3975(94)90269-0"},{"volume-title":"Proceedings of the 16th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., 279--290","author":"de Alfaro L.","unstructured":"de Alfaro , L. , Henzinger , T. , and Majumdar , R . 2001. From verification to control: dynamic programs for omega-regular objectives . In Proceedings of the 16th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., 279--290 . de Alfaro, L., Henzinger, T., and Majumdar, R. 2001. From verification to control: dynamic programs for omega-regular objectives. In Proceedings of the 16th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., 279--290.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","volume-title":"LNCS","volume":"85","author":"Emerson E.","unstructured":"Emerson , E. and Clarke , E . 1980. Characterizing correctness properties of parallel programs as fixpoints. In Colloquium on Automata, Languages and Programming (ICALP) , LNCS , Vol. 85 . Springer, Berlin, 169--181. Emerson, E. and Clarke, E. 1980. Characterizing correctness properties of parallel programs as fixpoints. In Colloquium on Automata, Languages and Programming (ICALP), LNCS, Vol. 85. Springer, Berlin, 169--181."},{"volume-title":"Symposium on Foundations of Computer Science (FOCS)","author":"Emerson E.","unstructured":"Emerson , E. and Jutla , C . 1988. The complexity of tree automata and logics of programs . In Symposium on Foundations of Computer Science (FOCS) . White Plains, New York, 328--337. Emerson, E. and Jutla, C. 1988. The complexity of tree automata and logics of programs. In Symposium on Foundations of Computer Science (FOCS). White Plains, New York, 328--337.","key":"e_1_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1137\/S0097539793304741"},{"key":"e_1_2_1_18_1","volume-title":"-L","author":"Emerson E.","year":"1986","unstructured":"Emerson , E. and Lei , C . -L . 1986 a. Efficient model checking in fragments of the propositional mu-calculus. In IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press , Washington, D.C., 267--278. Emerson, E. and Lei, C.-L. 1986a. Efficient model checking in fragments of the propositional mu-calculus. In IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Washington, D.C., 267--278."},{"key":"e_1_2_1_19_1","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS), B. Monien and G. Vidal-Naquet, Eds. LNCS","volume":"210","author":"Emerson E.","unstructured":"Emerson , E. and Lei , C . -L. 1986b. Temporal reasoning under generalized fairness constraints . In Symposium on Theoretical Aspects of Computer Science (STACS), B. Monien and G. Vidal-Naquet, Eds. LNCS , Vol. 210 . Springer, Orsay, France, 21--36. Emerson, E. and Lei, C.-L. 1986b. Temporal reasoning under generalized fairness constraints. In Symposium on Theoretical Aspects of Computer Science (STACS), B. Monien and G. Vidal-Naquet, Eds. LNCS, Vol. 210. Springer, Orsay, France, 21--36."},{"key":"e_1_2_1_20_1","volume-title":"Ed. LNCS","volume":"697","author":"Emerson E. A.","unstructured":"Emerson , E. A. , Jutla , C. S. , and Sistla , P . 1993. On model-checking for fragments of &mu;-calculus. In Computer Aided Verification, C. Courcoubetis , Ed. LNCS , Vol. 697 . Springer, Elounda, Greece, 385--396. Emerson, E. A., Jutla, C. S., and Sistla, P. 1993. On model-checking for fragments of &mu;-calculus. In Computer Aided Verification, C. Courcoubetis, Ed. LNCS, Vol. 697. Springer, Elounda, Greece, 385--396."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of Symposia in Applied Mathematics, 19--32","author":"Floyd R.","year":"1967","unstructured":"Floyd , R. 1967 . Mathematical aspects of computer science . In Proceedings of Symposia in Applied Mathematics, 19--32 . Floyd, R. 1967. Mathematical aspects of computer science. In Proceedings of Symposia in Applied Mathematics, 19--32."},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/363235.363259"},{"volume-title":"Proceedings of the American Control Conference","author":"Hoffmann G.","unstructured":"Hoffmann , G. and Wong-Toi , H . 1992. Symbolic synthesis of supervisory controllers . In Proceedings of the American Control Conference , Chicago, IL. Hoffmann, G. and Wong-Toi, H. 1992. Symbolic synthesis of supervisory controllers. In Proceedings of the American Control Conference, Chicago, IL.","key":"e_1_2_1_23_1"},{"volume-title":"Proceedings of the of the 40th IEEE Conference on Decision and Control","author":"Jiang S.","unstructured":"Jiang , S. and Kumar , R . 2001. Supervisory control of discrete event systems with CTL&ast; temporal logic specifications . In Proceedings of the of the 40th IEEE Conference on Decision and Control , Orlando, FL. Jiang, S. and Kumar, R. 2001. Supervisory control of discrete event systems with CTL&ast; temporal logic specifications. In Proceedings of the of the 40th IEEE Conference on Decision and Control, Orlando, FL.","key":"e_1_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1016\/S0020-0190(98)00150-1"},{"volume-title":"Automata, Logics, and Infinite Games---A Guide to Current Research","author":"Kirsten D.","unstructured":"Kirsten , D. 2002. Alternating tree automata and parity games . In Automata, Logics, and Infinite Games---A Guide to Current Research , E. Gr\u00e4del, W. Thomas, and T. Wilke, Eds. LNCS 2500. Springer , Heidelberg, 153--167. Kirsten, D. 2002. Alternating tree automata and parity games. In Automata, Logics, and Infinite Games---A Guide to Current Research, E. Gr\u00e4del, W. Thomas, and T. Wilke, Eds. LNCS 2500. Springer, Heidelberg, 153--167.","key":"e_1_2_1_26_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1007\/BF00264469"},{"doi-asserted-by":"crossref","unstructured":"Kumar R. and Garg V. 1995. Modeling and Control of Logical Discrete Event Systems. Kluwer Academic Publishers Dordrecht.  Kumar R. and Garg V. 1995. Modeling and Control of Logical Discrete Event Systems. Kluwer Academic Publishers Dordrecht.","key":"e_1_2_1_28_1","DOI":"10.1007\/978-1-4615-2217-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1016\/0020-0190(82)90065-5"},{"key":"e_1_2_1_30_1","volume-title":"Conference on Computer Aided Verification (CAV), D. Dill, Ed. LNCS","volume":"818","author":"Long D.","unstructured":"Long , D. , Browne , A. , Clarke , E. , Jha , S. , and Marrero , W . 1994. An improved algorithm for the evaluation of fixpoint expressions . In Conference on Computer Aided Verification (CAV), D. Dill, Ed. LNCS , Vol. 818 . Springer, Stanford, CA, USA, 338--350. Long, D., Browne, A., Clarke, E., Jha, S., and Marrero, W. 1994. An improved algorithm for the evaluation of fixpoint expressions. In Conference on Computer Aided Verification (CAV), D. Dill, Ed. LNCS, Vol. 818. Springer, Stanford, CA, USA, 338--350."},{"volume-title":"International Colloquium on Automata, Languages and Programming (ICALP)","author":"Niwi\u0144ski D.","unstructured":"Niwi\u0144ski , D. 1986. On fixed point clones . In International Colloquium on Automata, Languages and Programming (ICALP) , L. Kott, Ed. LNCS of Vol 226, Springer-Verlag , Berlin , 464--473. Niwi\u0144ski, D. 1986. On fixed point clones. In International Colloquium on Automata, Languages and Programming (ICALP), L. Kott, Ed. LNCS of Vol 226, Springer-Verlag, Berlin, 464--473.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","volume-title":"18th Annual Symposium on Foundations of Computer Science. IEEE","author":"Pnueli A.","year":"1977","unstructured":"Pnueli , A. 1977 . The temporal logic of programs . In 18th Annual Symposium on Foundations of Computer Science. IEEE , Providence, RI, 46--57. Pnueli, A. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science. IEEE, Providence, RI, 46--57."},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1137\/0325013"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1109\/5.21072"},{"key":"e_1_2_1_35_1","volume-title":"Symposium on Foundations of Computer Science (FOCS), 319--327","author":"Safra S.","year":"1988","unstructured":"Safra , S. 1988 . On the complexity of \u03c9-automata . In Symposium on Foundations of Computer Science (FOCS), 319--327 . Safra, S. 1988. On the complexity of \u03c9-automata. In Symposium on Foundations of Computer Science (FOCS), 319--327."},{"volume-title":"Texts in Theoretical Computer Science (EATCS Series)","author":"Schneider K.","unstructured":"Schneider , K. 2003. Verification of Reactive Systems---Formal Methods and Algorithms , Texts in Theoretical Computer Science (EATCS Series) . Springer , Berlin . Schneider, K. 2003. Verification of Reactive Systems---Formal Methods and Algorithms, Texts in Theoretical Computer Science (EATCS Series). Springer, Berlin.","key":"e_1_2_1_36_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1016\/0020-0190(96)00130-5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.2140\/pjm.1955.5.285"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1137\/S0363012991217536"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1137\/S0363012991217524"},{"key":"e_1_2_1_41_1","first-page":"2","article-title":"Alternating Tree Automata, Parity Games, and Modal &mu;-Calculus","volume":"8","author":"Wilke T.","year":"2001","unstructured":"Wilke , T. 2001 . Alternating Tree Automata, Parity Games, and Modal &mu;-Calculus . Bull. Soc. Math. Belg. 8 , 2 (May). Wilke, T. 2001. Alternating Tree Automata, Parity Games, and Modal &mu;-Calculus. Bull. Soc. Math. Belg. 8, 2 (May).","journal-title":"Bull. Soc. Math. Belg."},{"key":"e_1_2_1_42_1","volume-title":"Dept. of Electrical and Computer Engineering","author":"Wonham W. M.","year":"2004","unstructured":"Wonham , W. M. 2004. Supervisory control of discrete-event systems. Tech. rep ., Dept. of Electrical and Computer Engineering , University of Toronto . ECE 1636F\/1637S 2004 -05, http:\/\/www.control.utoronto.ca\/DES. Wonham, W. M. 2004. Supervisory control of discrete-event systems. Tech. rep., Dept. of Electrical and Computer Engineering, University of Toronto. ECE 1636F\/1637S 2004-05, http:\/\/www.control.utoronto.ca\/DES."},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1137\/0325036"},{"unstructured":"Ziller R. and Schneider K. 2003. A &mu;-calculus approach to supervisor synthesis. In GI\/ITG\/ GMM---Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. 132--143.  Ziller R. and Schneider K. 2003. A &mu;-calculus approach to supervisor synthesis. In GI\/ITG\/ GMM---Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. 132--143.","key":"e_1_2_1_44_1"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1067915.1067920","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1067915.1067920","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:26:19Z","timestamp":1750281979000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1067915.1067920"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,5]]}},"alternative-id":["10.1145\/1067915.1067920"],"URL":"https:\/\/doi.org\/10.1145\/1067915.1067920","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2005,5]]},"assertion":[{"value":"2005-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}