{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T19:40:04Z","timestamp":1748461204566,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662476659"},{"type":"electronic","value":"9783662476666"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-47666-6_2","type":"book-chapter","created":{"date-parts":[[2015,6,19]],"date-time":"2015-06-19T07:46:47Z","timestamp":1434700007000},"page":"11-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Automated Synthesis of Distributed Controllers"],"prefix":"10.1007","author":[{"given":"Anca","family":"Muscholl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,20]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL 2014, pp. 373\u2013384. ACM (2014)","DOI":"10.1145\/2578855.2535845"},{"key":"2_CR2","unstructured":"Akshay, S., Dinca, I., Genest, B., Stefanescu, A.: Implementing realistic asynchronous automata. In: FSTTCS 2013, LIPIcs, pp. 213\u2013224. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: LICS 1996, pp. 219\u2013228. IEEE (1996)","DOI":"10.1109\/LICS.1996.561322"},{"key":"2_CR4","unstructured":"Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf (2007)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-642-00596-1_29","volume-title":"Foundations of Software Science and Computational Structures","author":"B Bollig","year":"2009","unstructured":"Bollig, B., Grindei, M.-L., Habermehl, P.: Realizability of concurrent recursive programs. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 410\u2013424. Springer, Heidelberg (2009)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/978-3-642-39799-8_68","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2013","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951\u2013967. Springer, Heidelberg (2013)"},{"key":"2_CR7","unstructured":"Church, A.: Logic, arithmetics, and automata. In: Proceedings of the International Congress of Mathematicians (1962)"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1006\/inco.1993.1052","volume":"106","author":"R Cori","year":"1993","unstructured":"Cori, R., M\u00e9tivier, Y., Zielonka, W.: Asynchronous mappings and asynchronous cellular automata. Information and Computation 106, 159\u2013202 (1993)","journal-title":"Information and Computation"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-35179-2_2","volume":"6","author":"P Darondeau","year":"2012","unstructured":"Darondeau, P., Ricker, L.: Distributed control of discrete-event systems: A first step. Transactions on Petri Nets and Other Models of Concurrency 6, 24\u201345 (2012)","journal-title":"Transactions on Petri Nets and Other Models of Concurrency"},{"volume-title":"The Book of Traces","year":"1995","key":"2_CR10","unstructured":"Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)"},{"issue":"4","key":"2_CR11","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/BF00264611","volume":"27","author":"A Ehrenfeucht","year":"1989","unstructured":"Ehrenfeucht, A., Rozenberg, G.: Partial (set) 2-structures: Parts i and ii. Acta Informatica 27(4), 315\u2013368 (1989)","journal-title":"Acta Informatica"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 52\u201365. Springer, Heidelberg (2008)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS 2005, pp. 321\u2013330. IEEE (2005)","DOI":"10.1109\/LICS.2005.53"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-30538-5_23","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"P Gastin","year":"2004","unstructured":"Gastin, P., Lerman, B., Zeitoun, M.: Distributed games with causal memory are decidable for series-parallel systems. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 275\u2013286. Springer, Heidelberg (2004)"},{"issue":"2","key":"2_CR15","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2480759.2480761","volume":"14","author":"P Gastin","year":"2013","unstructured":"Gastin, P., Sznajder, N.: Fair synthesis for asynchronous distributed systems. ACM Transactions on Computational Logic 14(2), 9 (2013)","journal-title":"ACM Transactions on Computational Logic"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-14162-1_5","volume-title":"Automata, Languages and Programming","author":"B Genest","year":"2010","unstructured":"Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Optimal Zielonka-type construction of deterministic asynchronous automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 52\u201363. Springer, Heidelberg (2010)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-39212-2_26","volume-title":"Automata, Languages, and Programming","author":"B Genest","year":"2013","unstructured":"Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Asynchronous games over tree architectures. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 275\u2013286. Springer, Heidelberg (2013)"},{"issue":"6","key":"2_CR18","doi-asserted-by":"publisher","first-page":"920","DOI":"10.1016\/j.ic.2006.01.005","volume":"204","author":"B Genest","year":"2006","unstructured":"Genest, B., Kuske, D., Muscholl, A.: A Kleene theorem and model checking algorithms for existentially bounded communicating automata. Inf. Comput. 204(6), 920\u2013956 (2006)","journal-title":"Inf. Comput."},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/11787006_48","volume-title":"Automata, Languages and Programming","author":"B Genest","year":"2006","unstructured":"Genest, B., Muscholl, A.: Constructing exponential-size deterministic Zielonka automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 565\u2013576. Springer, Heidelberg (2006)"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01383879","volume":"2","author":"P Godefroid","year":"1993","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design 2(2), 149\u2013164 (1993)","journal-title":"Formal Methods in System Design"},{"issue":"6","key":"2_CR21","doi-asserted-by":"publisher","first-page":"1119","DOI":"10.1016\/j.jcss.2014.04.005","volume":"80","author":"J Gutierrez","year":"2014","unstructured":"Gutierrez, J., Winskel, G.: On the determinacy of concurrent games on event structures with infinite winning sets. J. Comput. Syst. Sci. 80(6), 1119\u20131137 (2014)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2004.08.004","volume":"202","author":"JG Henriksen","year":"2005","unstructured":"Henriksen, J.G., Mukund, M., Kumar, K.N., Sohoni, M., Thiagarajan, P.S.: A Theory of Regular MSC Languages. Inf. Comput. 202(1), 1\u201338 (2005)","journal-title":"Inf. Comput."},{"key":"2_CR23","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.tcs.2013.07.015","volume":"503","author":"S Krishna","year":"2013","unstructured":"Krishna, S., Muscholl, A.: A quadratic construction for Zielonka automata with acyclic communication structure. Theoretical Computer Science 503, 109\u2013114 (2013)","journal-title":"Theoretical Computer Science"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: LICS 2001, pp. 389\u2013398. IEEE (2001)","DOI":"10.1109\/LICS.2001.932514"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007, pp. 161\u2013170. IEEE (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"2_CR26","unstructured":"La Torre, S., Parlato, G.: Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. In: FSTTCS 2012, LIPIcs, pp. 173\u2013184. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)"},{"issue":"7","key":"2_CR27","first-page":"558","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Operating Systems 21(7), 558\u2013565 (1978)","journal-title":"Operating Systems"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-48224-5_33","volume-title":"Automata, Languages and Programming","author":"P Madhusudan","year":"2001","unstructured":"Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396\u2013407. Springer, Heidelberg (2001)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/11590156_16","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"P Madhusudan","year":"2005","unstructured":"Madhusudan, P., Thiagarajan, P.S., Yang, S.: The MSO theory of connectedly communicating processes. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 201\u2013212. Springer, Heidelberg (2005)"},{"key":"2_CR30","unstructured":"Mattern, F.: Virtual time and global states of distributed systems. In: International Workshop on Parallel and Distributed Algorithms, pp. 215\u2013226. Elsevier (1989)"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus (1977)","DOI":"10.7146\/dpb.v6i78.7691"},{"issue":"2\u20133","key":"2_CR32","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.tcs.2006.01.016","volume":"358","author":"P-A Melli\u00e8s","year":"2006","unstructured":"Melli\u00e8s, P.-A.: Asynchronous games 2: The true concurrency of innocence. TCS 358(2\u20133), 200\u2013228 (2006)","journal-title":"TCS"},{"issue":"3","key":"2_CR33","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/s004460050031","volume":"10","author":"M Mukund","year":"1997","unstructured":"Mukund, M., Sohoni, M.A.: Keeping track of the latest gossip in a distributed system. Distributed Computing 10(3), 137\u2013148 (1997)","journal-title":"Distributed Computing"},{"key":"2_CR34","unstructured":"Muscholl, A., Walukiewicz, I.: Distributed synthesis for acyclic architectures. In: FSTTCS 2014, LIPIcs, pp. 639\u2013651. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)"},{"issue":"4","key":"2_CR35","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/2591013","volume":"57","author":"M Odersky","year":"2014","unstructured":"Odersky, M., Rompf, T.: Unifying functional and object-oriented programming with Scala. Communications of the ACM 57(4), 76\u201386 (2014)","journal-title":"Communications of the ACM"},{"key":"2_CR36","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala. Artima (2010)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Peterson, G.L., Reif, J.H.: Multi-person alternation. In: FOCS 1979, pp. 348\u2013363. IEEE (1979)","DOI":"10.1109\/SFCS.1979.25"},{"key":"2_CR39","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS 1990. IEEE (1990)"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"2_CR41","doi-asserted-by":"crossref","DOI":"10.1090\/cbms\/013","volume-title":"Automata on Infinite Objects and Church\u2019s Problem","author":"MO Rabin","year":"1972","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Church\u2019s Problem. American Mathematical Society, Providence (1972)"},{"issue":"2","key":"2_CR42","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"P Ramadge","year":"1989","unstructured":"Ramadge, P., Wonham, W.: The control of discrete event systems. Proceedings of the IEEE 77(2), 81\u201398 (1989)","journal-title":"Proceedings of the IEEE"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"Sen, K., Vardhan, A., Agha, G., Rosu, G.: Decentralized runtime analysis of multithreaded applications. In: International Parallel and Distributed Processing Symposium (IPDPS 2006). IEEE (2006)","DOI":"10.1109\/IPDPS.2006.1639591"},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991)"},{"key":"2_CR45","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1051\/ita\/1987210200991","volume":"21","author":"W Zielonka","year":"1987","unstructured":"Zielonka, W.: Notes on finite asynchronous automata. RAIRO-Theoretical Informatics and Applications 21, 99\u2013135 (1987)","journal-title":"RAIRO-Theoretical Informatics and Applications"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-47666-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T19:03:32Z","timestamp":1748459012000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-47666-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662476659","9783662476666"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-47666-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"20 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}