{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:03:57Z","timestamp":1725577437948},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642180972"},{"type":"electronic","value":"9783642180989"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18098-9_28","type":"book-chapter","created":{"date-parts":[[2011,2,4]],"date-time":"2011-02-04T13:56:14Z","timestamp":1296827774000},"page":"261-271","source":"Crossref","is-referenced-by-count":13,"title":["State of B\u00fcchi Complementation"],"prefix":"10.1007","author":[{"given":"Ming-Hsien","family":"Tsai","sequence":"first","affiliation":[]},{"given":"Seth","family":"Fogarty","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Yih-Kuen","family":"Tsay","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 158\u2013174. Springer, Heidelberg (2010)"},{"issue":"2","key":"28_CR2","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1016\/j.tcs.2006.07.026","volume":"363","author":"C.S. Althoff","year":"2006","unstructured":"Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of B\u00fcchi automata. Theoretical Computer Science\u00a0363(2), 224\u2013233 (2006)","journal-title":"Theoretical Computer Science"},{"key":"28_CR3","first-page":"1","volume-title":"Proceedings of the International Congress on Logic, Method, and Philosophy of Science 1960","author":"J.R. B\u00fcchi","year":"1962","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science 1960, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"issue":"1:5","key":"28_CR4","first-page":"1","volume":"5","author":"L. Doyen","year":"2009","unstructured":"Doyen, L., Raskin, J.-F.: Antichains for the automata-based approach to model-checking. Logical Methods in Computer Science\u00a05(1:5), 1\u201320 (2009)","journal-title":"Logical Methods in Computer Science"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-642-00768-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Fogarty","year":"2009","unstructured":"Fogarty, S., Vardi, M.Y.: B\u00fcchi complementation and size-change termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 16\u201330. Springer, Heidelberg (2009)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-642-12002-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Fogarty","year":"2010","unstructured":"Fogarty, S., Vardi, M.Y.: Efficient B\u00fcchi universality checking. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 205\u2013220. Springer, Heidelberg (2010)"},{"issue":"4","key":"28_CR7","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. International Journal of Foundations of Computer Science\u00a017(4), 851\u2013868 (2006)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500. Springer, Heidelberg (2002)"},{"key":"28_CR9","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":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"724","DOI":"10.1007\/978-3-540-70575-8_59","volume-title":"Automata, Languages and Programming","author":"D. K\u00e4hler","year":"2008","unstructured":"K\u00e4hler, D., Wilke, T.: Complementation, disambiguation, and determinization of B\u00fcchi automata unified. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol.\u00a05125, pp. 724\u2013735. Springer, Heidelberg (2008)"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-04761-9_18","volume-title":"Automated Technology for Verification and Analysis","author":"H. Karmarkar","year":"2009","unstructured":"Karmarkar, H., Chakraborty, S.: On minimal odd rankings for B\u00fcchi complementation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 228\u2013243. Springer, Heidelberg (2009)"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-45315-6_18","volume-title":"Foundations of Software Science and Computation Structures","author":"V. King","year":"2001","unstructured":"King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 276\u2013286. Springer, Heidelberg (2001)"},{"key":"28_CR13","first-page":"358","volume-title":"FOCS","author":"N. Klarlund","year":"1991","unstructured":"Klarlund, N.: Progress measures for complementation of omega-automata with applications to temporal logic. In: FOCS, pp. 358\u2013367. IEEE, Los Alamitos (1991)"},{"issue":"2","key":"28_CR14","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J. Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic \u03c9-automata for formulas of linear temporal logic. Theoretical Computer Science\u00a0363(2), 182\u2013195 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"28_CR15","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 Transactions on Computational Logic\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"28_CR16","first-page":"531","volume-title":"FOCS","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531\u2013540. IEEE Computer Society, Los Alamitos (2005)"},{"key":"28_CR17","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. Manuscript CNET, Paris (1988)"},{"issue":"1&2","key":"28_CR18","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science\u00a0141(1&2), 69\u2013107 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"3:5","key":"28_CR19","first-page":"1","volume":"3","author":"N. Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science\u00a03(3:5), 1\u201321 (2007)","journal-title":"Logical Methods in Computer Science"},{"key":"28_CR20","first-page":"319","volume-title":"FOCS","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: FOCS, pp. 319\u2013327. IEEE, Los Alamitos (1988)"},{"key":"28_CR21","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: STACS. LIPIcs, vol.\u00a03, pp. 661\u2013672. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2009)"},{"key":"28_CR22","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 appplications to temporal logic. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"28_CR23","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":"28_CR24","doi-asserted-by":"publisher","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 revisited. In: Jewels are Forever, pp. 109\u2013120. Springer, Heidelberg (1999)"},{"key":"28_CR25","unstructured":"Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of B\u00fcchi complementation (full version), \n                  \n                    http:\/\/goal.im.ntu.edu.tw"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-78800-3_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.-K. Tsay","year":"2008","unstructured":"Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: GOAL extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 346\u2013350. Springer, Heidelberg (2008)"},{"key":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"28_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 137\u2013150. Springer, Heidelberg (2007)"},{"key":"28_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-70918-3_2","volume-title":"STACS 2007","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: The B\u00fcchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol.\u00a04393, pp. 12\u201322. Springer, Heidelberg (2007)"},{"key":"28_CR30","unstructured":"Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Logic and Automata: History and Perspective. Texts in Logic and Games, vol.\u00a02, pp. 629\u2013736. Amsterdam University Press, Amsterdam (2007)"},{"issue":"1:5","key":"28_CR31","first-page":"1","volume":"4","author":"Q. Yan","year":"2008","unstructured":"Yan, Q.: Lower bounds for complementation of omega-automata via the full automata technique. Logical Methods in Computer Science\u00a04(1:5), 1\u201320 (2008)","journal-title":"Logical Methods in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18098-9_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,24]],"date-time":"2019-03-24T06:28:53Z","timestamp":1553408933000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18098-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642180972","9783642180989"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18098-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}