{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T22:27:48Z","timestamp":1749421668409},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,9,23]],"date-time":"2016-09-23T00:00:00Z","timestamp":1474588800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"EU FP7 Programme (MEALS)","award":["295261"],"award-info":[{"award-number":["295261"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10626-016-0231-8","type":"journal-article","created":{"date-parts":[[2016,9,23]],"date-time":"2016-09-23T02:57:33Z","timestamp":1474599453000},"page":"109-142","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Maximally permissive controlled system synthesis for non-determinism and modal logic"],"prefix":"10.1007","volume":"27","author":[{"given":"A. C.","family":"van Hulst","sequence":"first","affiliation":[]},{"given":"M. A.","family":"Reniers","sequence":"additional","affiliation":[]},{"given":"W. J.","family":"Fokkink","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,23]]},"reference":[{"issue":"2","key":"231_CR1","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/s11225-009-9170-9","volume":"91","author":"L Alberucci","year":"2009","unstructured":"Alberucci L, Facchini A (2009) On modal \u03bc-calculus and G\u00f6del-L\u00f6b logic. Stud Logica 91(2):145\u2013169","journal-title":"Stud Logica"},{"key":"231_CR2","doi-asserted-by":"crossref","unstructured":"Antoniotti M, Mishra B (1995) Discrete event models + temporal logic = supervisory controller: automatic synthesis of locomotion controllers. In: Proceedings of robotics and automation, IEEE, pp 1441\u2013 1446","DOI":"10.1109\/ROBOT.1995.525480"},{"key":"231_CR3","unstructured":"Arnold A, Walukiewicz I (2008) Nondeterministic controllers of nondeterministic processes. In: Proceedings of logic and automata, Amsterdam University Press, pp 29\u201352"},{"issue":"1","key":"231_CR4","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S0304-3975(02)00442-5","volume":"303","author":"A Arnold","year":"2003","unstructured":"Arnold A, Vincent A, Walukiewicz I (2003) Games for synthesis of controllers with partial observation. Theor Comput Sci 303(1):7\u201334","journal-title":"Theor Comput Sci"},{"key":"231_CR5","doi-asserted-by":"crossref","unstructured":"Baeten J, Basten T, Reniers M (2010) Process algebra: equational theories of communicating processes. Cambridge University Press","DOI":"10.1017\/CBO9781139195003"},{"key":"231_CR6","doi-asserted-by":"crossref","unstructured":"Basu S, Kumar R (2007) Quotient-based control synthesis for partially observed non-deterministic plants with mu-calculus specifications. In: Proceedings of CDC, IEEE, pp 5294\u2013 5299","DOI":"10.1109\/CDC.2007.4434955"},{"key":"231_CR7","doi-asserted-by":"crossref","unstructured":"Bull R, Segerberg K (2001) Basic modal logic. In: Handbook of philosophical logic, Springer, pp 1\u201381","DOI":"10.1007\/978-94-017-0454-0_1"},{"key":"231_CR8","doi-asserted-by":"crossref","unstructured":"Cassandras C, Lafortune S (2008) Introduction to discrete event systems. Springer","DOI":"10.1007\/978-0-387-68612-7"},{"issue":"2","key":"231_CR9","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland R, Steffen B (1993) A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design 2(2):121\u2013147","journal-title":"Formal Methods in System Design"},{"key":"231_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito N, Braberman V, Piterman N, Uchitel S (2010) Synthesis of live behaviour models. In: Proceedings of FSE, ACM, pp 77\u201386","DOI":"10.1145\/1882291.1882305"},{"issue":"1","key":"231_CR11","first-page":"9","volume":"22","author":"N D\u2019Ippolito","year":"2013","unstructured":"D\u2019Ippolito N, Braberman V, Piterman N, Uchitel S (2013) Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans Softw Eng Methodol 22(1):9","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"231_CR12","doi-asserted-by":"crossref","unstructured":"Ehlers R, Lafortune S, Tripakis S, Vardi M (2014) Bridging the gap between supervisory control and reactive synthesis: case of full observation and centralized control. In: Proceedings of WODES, IFAC, pp 222\u2013227","DOI":"10.3182\/20140514-3-FR-4046.00018"},{"issue":"1","key":"231_CR13","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/S0947-3580(97)70063-3","volume":"3","author":"M Fabian","year":"1997","unstructured":"Fabian M, Lennartson B (1997) A class of non-deterministic specifications for supervisory control. Eur J Control 3(1):81\u201390","journal-title":"Eur J Control"},{"key":"231_CR14","unstructured":"Fainekos G, Girard A, Pappas G (1994) Hierarchical synthesis of hybrid controllers from temporal logic specifications. In: Proceedings of HSCC, Springer, pp 203\u2013216"},{"key":"231_CR15","doi-asserted-by":"crossref","unstructured":"van Glabbeek R (1993) The linear time branching time spectrum II. In: Proceedings of CONCUR, Springer, pp 66\u201381","DOI":"10.1007\/3-540-57208-2_6"},{"key":"231_CR16","doi-asserted-by":"crossref","unstructured":"Havelund K, Larsen K, Skou A (1999) Formal verification of a power controller using the real-time model checker UPPAAL. In: Proceedings of AMAST, Springer, pp 277\u2013298","DOI":"10.7146\/brics.v6i8.20065"},{"issue":"1","key":"231_CR17","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32(1):137\u2013161","journal-title":"J ACM"},{"key":"231_CR18","unstructured":"van Hulst A, Reniers M, Fokkink W (2014) Maximal synthesis for Hennessy-Milner logic. ACM Trans Embed Comput Syst 14(1):10:1\u201310:21"},{"key":"231_CR19","doi-asserted-by":"crossref","unstructured":"van Hulst A, Reniers M, Fokkink W (2015) Maximally permissive controlled system synthesis for modal logic. In: Proceedings of SOFSEM, Springer, vol 8939, pp 230\u2013241","DOI":"10.1007\/978-3-662-46078-8_19"},{"key":"231_CR20","unstructured":"Jansen S (2014) Design and implementation of model-based controllers for baggage handling systems. TU\/e master thesis archive at http:\/\/www.tue.nl"},{"key":"231_CR21","doi-asserted-by":"crossref","unstructured":"Jessen J, Rasmussen J, Larsen K, David A (2007) Guided controller synthesis for climate controller using UPPAAL Tiga. In: Proceedings of FORMATS, Springer, vol 4763, pp 227\u2013 240","DOI":"10.1007\/978-3-540-75454-1_17"},{"issue":"6","key":"231_CR22","doi-asserted-by":"crossref","first-page":"2079","DOI":"10.1137\/S0363012902409982","volume":"44","author":"S Jiang","year":"2006","unstructured":"Jiang S, Kumar R (2006) Supervisory control of discrete event systems with CTL* temporal logic specifications. SIAM J Control Optim 44(6):2079\u20132103","journal-title":"SIAM J Control Optim"},{"key":"231_CR23","unstructured":"Kamphuis R (2013) Design and real-time implementation of a supervisory controller for a part of veghel airport. TU\/e master thesis archive at http:\/\/www.tue.nl"},{"key":"231_CR24","doi-asserted-by":"crossref","unstructured":"Kumar R, Shayman M (1994) Non-blocking supervisory control of nondeterministic discrete event systems. In: Proceedings of ACC, IEEE, pp 1089\u20131093","DOI":"10.1109\/ACC.1994.751915"},{"key":"231_CR25","doi-asserted-by":"crossref","unstructured":"Kupferman O, Vardi M (2000) \u03bc-calculus synthesis. In: Proceedings of MFCS, Springer, pp 497\u2013507","DOI":"10.1007\/3-540-44612-5_45"},{"key":"231_CR26","doi-asserted-by":"crossref","unstructured":"Kupferman O, Madhusudan P, Thiagarajan P, Vardi M (2000) Open systems in reactive environments: control and synthesis. In: Proceedings of CONCUR, Springer, pp 92\u2013107","DOI":"10.1007\/3-540-44618-4_9"},{"key":"231_CR27","unstructured":"Markovski J (2011) A process-theoretic approach to supervisory control theory. In: Proceedings of ACC, IEEE, pp 4496\u20134501"},{"key":"231_CR28","doi-asserted-by":"crossref","unstructured":"Markovski J, Jacobs K, van Beek D, Somers L, Rooda J (2010) Coordination of resources using generalized state-based requirements. In: Proceedings of WODES, pp 287\u2013292","DOI":"10.3182\/20100830-3-DE-4013.00048"},{"key":"231_CR29","doi-asserted-by":"crossref","unstructured":"McMillan K (1993) Symbolic model checking. Springer","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"231_CR30","doi-asserted-by":"crossref","unstructured":"Moor T, Davoren J (2001) Robust controller synthesis for hybrid systems using modal logic. In: Proceedings of HSCC, Springer, pp 433\u2013446","DOI":"10.1007\/3-540-45351-2_35"},{"key":"231_CR31","unstructured":"Mushtaq F (2000) The safe design of computer controlled pipeless batch plants. PhD thesis, Loughborough University"},{"key":"231_CR32","doi-asserted-by":"crossref","unstructured":"Ostroff J (1989) Synthesis of controllers for real-time discrete event systems. In: Proceedings of CDC, IEEE, pp 138\u2013144","DOI":"10.1109\/CDC.1989.70091"},{"key":"231_CR33","doi-asserted-by":"crossref","unstructured":"Pinchinat S (2005) You can always compute maximally permissive controllers under partial observation when they exist. In: Proceedings of ACC, IEEE, pp 2287\u20132292","DOI":"10.1109\/ACC.2005.1470310"},{"key":"231_CR34","doi-asserted-by":"crossref","unstructured":"Pinchinat S, Raclet J (2005) Supervisory control problems for nondeterministic discrete-event systems: a logical approach. In: Proceedings of the IFAC world congress, Elsevier, vol 16, pp 295\u2013301","DOI":"10.3182\/20050703-6-CZ-1902.00296"},{"key":"231_CR35","unstructured":"Pinchinat S, Riedweg S (2003) Quantified mu-calculus for control synthesis. In: Proceedings of MFCS. Springer, pp 642\u2013651"},{"key":"231_CR36","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of POPL, ACM, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"231_CR37","unstructured":"Pralet C, Verfaillie G, Lema\u00eetre M, Infantes G (2010) Constraint-based controller synthesis in non-deterministic and partially observable domains. In: Proceedings of ECAI, IOS Press, vol 215, pp 681\u2013686"},{"issue":"1","key":"231_CR38","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P Ramadge","year":"1987","unstructured":"Ramadge P, Wonham M (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25(1):206\u2013230","journal-title":"SIAM J Control Optim"},{"key":"231_CR39","doi-asserted-by":"crossref","unstructured":"Rutten J (2000) Coalgebra, concurrency, and control. In: Discrete event systems: analysis and control. Springer, pp 31\u201338","DOI":"10.1007\/978-1-4615-4493-7_2"},{"key":"231_CR40","doi-asserted-by":"crossref","unstructured":"Sokolsky O, Smolka S (1994) Incremental model checking in the modal mu-calculus. In: Proceedings of CAV, Springer, pp 351\u2013363","DOI":"10.1007\/3-540-58179-0_67"},{"key":"231_CR41","doi-asserted-by":"crossref","unstructured":"Su R (2008) Supervisor synthesis based on abstractions of nondeterministic automata. In: Proceedings of WODES, IEEE, pp 412\u2013418","DOI":"10.1109\/WODES.2008.4605981"},{"key":"231_CR42","doi-asserted-by":"crossref","unstructured":"Wolff E, Topcu U, Murray R (2013) Efficient reactive controller synthesis for a fragment of linear temporal logic. In: Proceedings of ICRA, IEEE, pp 5033\u20135040","DOI":"10.1109\/ICRA.2013.6631296"},{"issue":"2","key":"231_CR43","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/1067915.1067920","volume":"4","author":"R Ziller","year":"2005","unstructured":"Ziller R, Schneider K (2005) Combining supervisor synthesis and model checking. ACM Trans Embed Comput Syst 4(2):331\u2013362","journal-title":"ACM Trans Embed Comput Syst"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-016-0231-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-016-0231-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-016-0231-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T22:47:04Z","timestamp":1568414824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-016-0231-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,23]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["231"],"URL":"https:\/\/doi.org\/10.1007\/s10626-016-0231-8","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,23]]}}}