{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:54:57Z","timestamp":1760079297534},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540709176"},{"type":"electronic","value":"9783540709183"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70918-3_2","type":"book-chapter","created":{"date-parts":[[2007,5,23]],"date-time":"2007-05-23T23:41:23Z","timestamp":1179963683000},"page":"12-22","source":"Crossref","is-referenced-by-count":37,"title":["The B\u00fcchi Complementation Saga"],"prefix":"10.1007","author":[{"given":"Moshe Y.","family":"Vardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., et al.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 296\u2013311. Springer, Heidelberg (2002)"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(93)90160-U","volume":"119","author":"J.C. Birget","year":"1993","unstructured":"Birget, J.C.: Partial orders on words, minimal elements of regular languages, and state complexity. Theoretical Computer Science\u00a0119, 267\u2013291 (1993)","journal-title":"Theoretical Computer Science"},{"key":"2_CR3","first-page":"1","volume-title":"Proc. International Congress on Logic, Method, and Philosophy of Science","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Method, and Philosophy of Science, 1960, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"issue":"2","key":"2_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"N. Daniele","year":"1999","unstructured":"Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: Proc. 7th InternationalColloq. on Automata, Languages and Programming, pp. 169\u2013181 (1980)","DOI":"10.1007\/3-540-10003-2_69"},{"key":"2_CR7","volume-title":"Proc. 18th Hawaii International Conference on System Sciences","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Lei, C.-L.: Temporal model checking under generalized fairness constraints. In: Proc. 18th Hawaii International Conference on System Sciences, Western Periodicals Company, North Holywood (1985)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., et al.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"issue":"4","key":"2_CR9","doi-asserted-by":"publisher","first-page":"851","DOI":"10.1142\/S0129054106004145","volume":"17","author":"E. Friedgut","year":"2006","unstructured":"Friedgut, E., Kupferman, O., Vardi, M.Y.: B\u00fcchi complementation made tighter. Int\u2019l J. of Foundations of Computer Science\u00a017(4), 851\u2013867 (2006)","journal-title":"Int\u2019l J. of Foundations of Computer Science"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"2_CR11","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":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., et al.: On complementing nondeterministic B\u00fcchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 96\u2013110. Springer, Heidelberg (2003)"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1006\/inco.2001.3085","volume":"173","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Information and Computation\u00a0173(1), 64\u201381 (2002)","journal-title":"Information and Computation"},{"issue":"5","key":"2_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering, Special issue on Formal Methods in Software Practice\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"2_CR16","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1109\/SFCS.1991.185391","volume-title":"Proc. 32nd IEEE Symp. on Foundations of Computer Science","author":"N. Klarlund","year":"1991","unstructured":"Klarlund, N.: Progress measures for complementation of \u03c9-automata with applications to temporal logic. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, San Juan, October 1991, pp. 358\u2013367. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1109\/ISTCS.1997.595167","volume-title":"Proc. 5th Israeli Symp. on Theory of Computing and Systems","author":"O. Kupferman","year":"1997","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: Proc. 5th Israeli Symp. on Theory of Computing and Systems, pp. 147\u2013158. IEEE Computer Society Press, Los Alamitos (1997)"},{"issue":"2","key":"2_CR18","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 Trans. on Computational Logic\u00a02(2), 408\u2013429 (2001)","journal-title":"ACM Trans. on Computational Logic"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/978-3-540-31980-1_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Complementation constructions for nondeterministic automata on infinite words. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 206\u2013221. Springer, Heidelberg (2005)"},{"key":"2_CR20","first-page":"591","volume":"305","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. Theoretical Computer Science\u00a0305, 591\u2013606 (2005)","journal-title":"Theoretical Computer Science"},{"key":"2_CR21","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 University Press, Princeton (1994)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"C. L\u00f6ding","year":"1999","unstructured":"L\u00f6ding, C.: Optimal bounds for the transformation of omega-automata. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 97\u2013109. Springer, Heidelberg (1999)"},{"key":"2_CR23","unstructured":"Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)"},{"key":"2_CR24","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. Theoretical Computer Science\u00a032, 321\u2013330 (1984)","journal-title":"Theoretical Computer Science"},{"key":"2_CR25","first-page":"3","volume-title":"Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical design","author":"D.E. Muller","year":"1963","unstructured":"Muller, D.E.: Infinite sequences and finite machines. In: Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical design, pp. 3\u201316. IEEE Computer Society Press, Los Alamitos (1963)"},{"key":"2_CR26","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. Theoretical Computer Science\u00a054, 267\u2013276 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"2_CR27","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(86)90136-2","volume":"47","author":"J.P. P\u00e9cuchet","year":"1986","unstructured":"P\u00e9cuchet, J.P.: On the complementation of b\u00fcchi automata. Theor. Comput. Sci.\u00a047(3), 95\u201398 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR28","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":"2_CR29","first-page":"319","volume-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, White Plains, October 1988, pp. 319\u2013327. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"2_CR30","volume-title":"Proc. 24th ACM Symp. on Theory of Computing","author":"S. Safra","year":"1992","unstructured":"Safra, S.: Exponential determinization for \u03c9-automata with strong-fairness acceptance condition. In: Proc. 24th ACM Symp. on Theory of Computing, Victoria, May 1992, ACM Press, New York (1992)"},{"key":"2_CR31","first-page":"275","volume-title":"Proc. 10th ACM Symp. on Theory of Computing","author":"W. Sakoda","year":"1978","unstructured":"Sakoda, W., Sipser, M.: Non-determinism and the size of two-way automata. In: Proc. 10th ACM Symp. on Theory of Computing, pp. 275\u2013286. ACM Press, New York (1978)"},{"key":"2_CR32","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theoretical Computer Science\u00a049, 217\u2013237 (1987)","journal-title":"Theoretical Computer Science"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"2_CR34","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1002\/sapm1993893233","volume":"89","author":"N.M. Temme","year":"1993","unstructured":"Temme, N.M.: Asimptotic estimates of Stirling numbers. Stud. Appl. Math.\u00a089, 233\u2013243 (1993)","journal-title":"Stud. Appl. Math."},{"key":"2_CR35","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/978-3-642-60207-8_10","volume-title":"Jewels are Forever","author":"W. Thomas","year":"1999","unstructured":"Thomas, W.: Complementation of B\u00fcchi automata revised. In: Karhum\u00e4ki, J., et al. (eds.) Jewels are Forever, pp. 109\u2013120. Springer, Heidelberg (1999)"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"M.Y. Vardi","year":"1991","unstructured":"Vardi, M.Y.: Verification of concurrent programs - the automata-theoretic framework. Annals of Pure and Applied Logic\u00a051, 79\u201398 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"2_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"issue":"1\u20132","key":"2_CR38","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056(1\u20132), 72\u201399 (1983)","journal-title":"Information and Control"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/11787006_50","volume-title":"Automata, Languages and Programming","author":"Q. Yan","year":"2006","unstructured":"Yan, Q.: Lower bounds for complementation of \u03c9-automata via the full automata technique. In: Bugliesi, M., et al. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 589\u2013600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","STACS 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70918-3_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:11:47Z","timestamp":1605762707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70918-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540709176","9783540709183"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70918-3_2","relation":{},"subject":[]}}