{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:26:00Z","timestamp":1746001560900},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_14","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:44:59Z","timestamp":1278888299000},"page":"206-221","source":"Crossref","is-referenced-by-count":20,"title":["Complementation Constructions for Nondeterministic Automata on Infinite Words"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. TCS\u00a082(2), 253\u2013284 (1991)","journal-title":"TCS"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Attie, P.: Liveness-preserving simulation relations. In: Proc. 18th PODC, pp. 63\u201372 (1999)","DOI":"10.1145\/301308.301328"},{"key":"14_CR3","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, Stanford, pp. 1\u201312 (1962)"},{"key":"14_CR4","first-page":"117","volume":"8","author":"Y. Choueka","year":"1974","unstructured":"Choueka, Y.: Theories of automata on \u03c9-tapes: A simplified approach. Journal of CSS\u00a08, 117\u2013141 (1974)","journal-title":"Journal of CSS"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","first-page":"255","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1991","unstructured":"Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation relations. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 255\u2013265. Springer, Heidelberg (1991)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.: Tree automata, \u03bc-calculus and determinacy. In: Proc. 32nd FOCS, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"14_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":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-30476-0_10","volume-title":"Automated Technology for Verification and Analysis","author":"E. Friedgut","year":"2004","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol.\u00a03299, pp. 64\u201378. Springer, Heidelberg (2004)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/3-540-45657-0_51","volume-title":"Computer Aided Verification","author":"S. Gurumurthy","year":"2002","unstructured":"Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 610\u2013623. Springer, Heidelberg (2002)"},{"key":"14_CR10","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":"14_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453\u2013462 (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"issue":"9","key":"14_CR13","first-page":"889","volume":"28","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kupferman, O.: On the behavioral inheritance of state-based objects. IEEE TSE\u00a028(9), 889\u2013903 (2002)","journal-title":"IEEE TSE"},{"issue":"1","key":"14_CR14","first-page":"64","volume":"173","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. I&C\u00a0173(1), 64\u201381 (2002)","journal-title":"I&C"},{"issue":"5","key":"14_CR15","first-page":"279","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE TSE\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE TSE"},{"key":"14_CR16","unstructured":"Klarlund, N.: Progress Measures and finite arguments for infinite computations. PhD thesis, Cornell University (1990)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Klarlund, N.: Progress measures for complementation of \u03c9-automata with applications to temporal logic. In: Proc. 32nd FOCS, pp. 358\u2013367 (1991)","DOI":"10.1109\/SFCS.1991.185391"},{"issue":"1","key":"14_CR18","first-page":"203","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. I&C\u00a0163(1), 203\u2013243 (2000)","journal-title":"I&C"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-45069-6_36","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"2003","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace containment. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 381\u2013393. Springer, Heidelberg (2003)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 - Concurrency Theory","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariant in action. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013115. Springer, Heidelberg (2002)"},{"key":"14_CR21","first-page":"59","volume":"35","author":"R.P. Kurshan","year":"1987","unstructured":"Kurshan, R.P.: Complementing deterministic B\u00fcchi automata in polynomial time. Journal of CSS\u00a035, 59\u201371 (1987)","journal-title":"Journal of CSS"},{"key":"14_CR22","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)"},{"key":"14_CR23","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM ToCL\u00a02, 408\u2013429 (2001)","journal-title":"ACM ToCL"},{"key":"14_CR24","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":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume-title":"Automata, Languages and Programming","author":"D. Lehman","year":"1981","unstructured":"Lehman, D., Pnueli, A., Stavi, J.: Impartiality, justice, and fairness \u2013 the ethics of concurrent termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol.\u00a0115, pp. 264\u2013277. Springer, Heidelberg (1981)"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proc. 6th PODC, pp. 137\u2013151 (1987)","DOI":"10.1145\/41840.41852"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-44659-1_26","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Merz","year":"2000","unstructured":"Merz, S.: Weak alternating automata in Isabelle\/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 423\u2013440. Springer, Heidelberg (2000)"},{"key":"14_CR28","volume-title":"Complementation is more difficult with automata on infinite words","author":"M. Michel","year":"1988","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time: Preliminary report. In: Proc. 5th STOC, pp. 1\u20139 (1973)","DOI":"10.1145\/800125.804029"},{"key":"14_CR30","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. TCS\u00a054, 267\u2013276 (1987)","journal-title":"TCS"},{"key":"14_CR31","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1147\/rd.32.0114","volume":"3","author":"M.O. Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development\u00a03, 115\u2013125 (1959)","journal-title":"IBM Journal of Research and Development"},{"key":"14_CR32","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":"14_CR33","doi-asserted-by":"crossref","unstructured":"Safra, S.: Exponential determinization for \u03c9-automata with strong-fairness acceptance condition. In: Proc. 24th STOC (1992)","DOI":"10.1145\/129712.129739"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Safra, S., Vardi, M.Y.: On \u03c9-automata and temporal logic. In: Proc. 21st STOC, pp. 127\u2013137 (1989)","DOI":"10.1145\/73007.73019"},{"key":"14_CR35","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 \u03c9-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 261\u2013277. Springer, Heidelberg (1995)"},{"issue":"1","key":"14_CR36","first-page":"1","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C\u00a0115(1), 1\u201337 (1994)","journal-title":"I&C"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:32:42Z","timestamp":1605760362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}