{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:16:17Z","timestamp":1775873777711,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662460771","type":"print"},{"value":"9783662460788","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46078-8_19","type":"book-chapter","created":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T09:54:29Z","timestamp":1421229269000},"page":"230-241","source":"Crossref","is-referenced-by-count":5,"title":["Maximally Permissive Controlled System Synthesis for Modal Logic"],"prefix":"10.1007","author":[{"given":"Alan C.","family":"van Hulst","sequence":"first","affiliation":[]},{"given":"Michel A.","family":"Reniers","sequence":"additional","affiliation":[]},{"given":"Wan J.","family":"Fokkink","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-35743-5_4","volume-title":"Formal Aspects of Component Software","author":"B. Aminof","year":"2012","unstructured":"Aminof, B., Mogavero, F., Murano, A.: Synthesis of hierarchical systems. In: Arbab, F., \u00d6lveczky, P.C. (eds.) FACS 2011. LNCS, vol.\u00a07253, pp. 42\u201360. Springer, Heidelberg (2012)"},{"issue":"303","key":"19_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S0304-3975(02)00442-5","volume":"1","author":"A. Arnold","year":"2003","unstructured":"Arnold, A., Vincent, I., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theoretical Computer Science\u00a01(303), 7\u201334 (2003)","journal-title":"Theoretical Computer Science"},{"key":"19_CR3","unstructured":"Arnold, A., Walukiewicz, I.: Nondeterministic controllers of nondeterministic processes. In: Logic and Automata, pp. 29\u201352. Amsterdam University Press (2008)"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Baeten, J., van Beek, B., van Hulst, A., Markovski, J.: A process algebra for supervisory coordination. In: Process Algebra and Coordination. EPTCS, pp. 36\u201355 (2011)","DOI":"10.4204\/EPTCS.60.3"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Bull, R., Segerberg, K.: Basic modal logic. In: Handbook of Philosophical Logic, pp. 1\u201388. Springer (1994)","DOI":"10.1007\/978-94-009-6259-0_1"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Cassandras, C., Lafortune, S.: Introduction to Discrete Event Systems. Springer (1999)","DOI":"10.1007\/978-1-4757-4070-7"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design\u00a02, 121\u2013147 (1993)","journal-title":"Formal Methods in System Design"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behaviour models. In: Foundations of Software Engineering, pp. 77\u201386. ACM Press (2010)","DOI":"10.1145\/1882291.1882305"},{"issue":"1","key":"19_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2430536.2430543","volume":"22","author":"N. D\u2019Ippolito","year":"2013","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesizing nonanomalous event-based controllers for liveness goals. ACM Transactions on Software Engineering Methodology\u00a022(1), 1\u201336 (2013)","journal-title":"ACM Transactions on Software Engineering Methodology"},{"issue":"1","key":"19_CR10","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM\u00a032(1), 137\u2013161 (1985)","journal-title":"Journal of the ACM"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Lustig, Y., Vardi, M.: Synthesis from recursive-components libraries. In: Games, Automata, Logics and Formal Verification. EPTCS, pp. 1\u201316 (2011)","DOI":"10.4204\/EPTCS.54.1"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Principles of Programming Languages, pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1","key":"19_CR13","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P. Ramadge","year":"1987","unstructured":"Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM Journal on Control and Optimization\u00a025(1), 206\u2013230 (1987)","journal-title":"SIAM Journal on Control and Optimization"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-58179-0_67","volume-title":"Computer Aided Verification","author":"O. Sokolsky","year":"1994","unstructured":"Sokolsky, O., Smolka, S.: Incremental model checking in the modal mu-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 351\u2013363. Springer, Heidelberg (1994)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"R. Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.: The linear time-branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 66\u201381. Springer, Heidelberg (1993)"},{"key":"19_CR16","unstructured":"van Hulst, A.: Coq v8.3 proofs (2014), http:\/\/seweb.se.wtb.tue.nl\/~ahulst\/sofsem\/"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"van Hulst, A., Reniers, M., Fokkink, W.: Maximal synthesis for Hennessy-Milner logic. In: Application of Concurrency to System Design, pp. 1\u201310. IEEE (2013)","DOI":"10.1109\/ACSD.2013.4"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"van Hulst, A., Reniers, M., Fokkink, W.: Maximal synthesis for Hennessy-Milner logic with the box-modality. In: Workshop on Discrete Event Systems, pp. 278\u2013285. IEEE (2014)","DOI":"10.3182\/20140514-3-FR-4046.00034"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"van Hulst, A., Reniers, M., Fokkink, W.: Maximally permissive controlled system synthesis for modal logic (2014), preprint at http:\/\/arxiv.org\/abs\/1408.3317\/","DOI":"10.1007\/978-3-662-46078-8_19"},{"issue":"2","key":"19_CR20","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1145\/1067915.1067920","volume":"4","author":"R. Ziller","year":"2005","unstructured":"Ziller, R., Schneider, K.: Combining supervisory synthesis and model checking. ACM Transactions on Embedded Computing Systems\u00a04(2), 331\u2013362 (2005)","journal-title":"ACM Transactions on Embedded Computing Systems"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2015: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46078-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,26]],"date-time":"2022-04-26T16:48:30Z","timestamp":1650991710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46078-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460771","9783662460788"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46078-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}