{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:23Z","timestamp":1763467763476},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_6","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T01:07:51Z","timestamp":1154740071000},"page":"31-44","source":"Crossref","is-referenced-by-count":65,"title":["Safraless Compositional Synthesis"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Automata, Languages and Programming","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable concurrent program specifications. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 1\u201317. Springer, Heidelberg (1989)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11605157_22","volume-title":"Implementation and Application of Automata","author":"C.S. Althoff","year":"2006","unstructured":"Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of b\u00fcchi automata. In: Farr\u00e9, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol.\u00a03845, pp. 262\u2013272. Springer, Heidelberg (2006)"},{"key":"6_CR3","first-page":"117","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: A simplified approach. JCSS\u00a08, 117\u2013141 (1974)","journal-title":"JCSS"},{"key":"6_CR4","unstructured":"Church, A.: Logic, arithmetics, and automata. In: ICM 1962, pp. 23\u201335 (1963)"},{"key":"6_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"6_CR6","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace theory for automatic hierarchical verification of speed independent circuits","author":"D.L. Dill","year":"1989","unstructured":"Dill, D.L.: Trace theory for automatic hierarchical verification of speed independent circuits. MIT Press, Cambridge (1989)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"Computer Aided Verification","author":"J. Elgaard","year":"1998","unstructured":"Elgaard, J., Klarlund, N., M\u00f6ller, A.: Mona 1.x: new techniques for WS1S and WS2S. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 516\u2013520. Springer, Heidelberg (1998)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/3-540-15648-8_7","volume-title":"Logics of Programs","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A.: Automata, tableaux, and temporal logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 79\u201387. Springer, Heidelberg (1985)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing, and Verification, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research","author":"E. Gr\u00e4del","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500. Springer, Heidelberg (2002)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-39724-3_10","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Gurumurthy","year":"2003","unstructured":"Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-31980-1_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Harding","year":"2005","unstructured":"Harding, A., Ryan, M., Schobbens, P.Y.: A new algorithm for strategy synthesis in ltl games. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 477\u2013492. Springer, Heidelberg (2005)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M. Jurzi\u0144Ski","year":"2000","unstructured":"Jurzi\u0144Ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol.\u00a01770, pp. 290\u2013301. Springer, Heidelberg (2000)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-540-24730-2_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Kupferman","year":"2004","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 591\u2013606. Springer, Heidelberg (2004)"},{"key":"6_CR15","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th FOCS (2005)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: 12th POPL, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"6_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"6_CR18","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. TCS\u00a032, 321\u2013330 (1984)","journal-title":"TCS"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-16066-3_15","volume-title":"Computation Theory","author":"A.W. Mostowski","year":"1985","unstructured":"Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) SCT 1984. LNCS, vol.\u00a0208, pp. 157\u2013168. Springer, Heidelberg (1985)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"D.E. Muller","year":"1986","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol.\u00a0226. Springer, Heidelberg (1986)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: 25th LICS (to appear, 2006)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Saar, Y.: Design synthesis in action: Solving a 2exptime-complete problem in n\n                           3. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Weakly definable relations and special automata. In: Symp. Math. Logic and Foundations of Set Theory, pp. 1\u201323 (1970)","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Automata on infinite objects and Church\u2019s problem. In: AMS (1972)","DOI":"10.1090\/cbms\/013"},{"key":"6_CR26","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: 29th FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Safra, S.: Exponential determinization for \u03c9-automata with strong-fairness acceptance condition. In: 24th STOC (1992)","DOI":"10.1145\/129712.129739"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-60385-9_16","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Tasiran","year":"1995","unstructured":"Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic omega-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 261\u2013277. Springer, Heidelberg (1995)"},{"issue":"2","key":"6_CR30","first-page":"182","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. JCSS\u00a032(2), 182\u2013221 (1986)","journal-title":"JCSS"},{"issue":"1","key":"6_CR31","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. IC\u00a0115(1), 1\u201337 (1994)","journal-title":"IC"},{"key":"6_CR32","first-page":"360","volume-title":"19th DAC","author":"J. Yang","year":"2001","unstructured":"Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. In: 19th DAC, pp. 360\u2013367. IEEE, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:35:54Z","timestamp":1558294554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11817963_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}