{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:57:54Z","timestamp":1770753474574,"version":"3.50.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,5,1]],"date-time":"2014-05-01T00:00:00Z","timestamp":1398902400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["(279307: Graph Games)"],"award-info":[{"award-number":["(279307: Graph Games)"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P 23499-N23"],"award-info":[{"award-number":["P 23499-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11407-N23 (RiSE)"],"award-info":[{"award-number":["S11407-N23 (RiSE)"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT10-002"],"award-info":[{"award-number":["ICT10-002"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006112","name":"Microsoft Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006112","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2014,5]]},"abstract":"<jats:p>\n            The computation of the winning set for B\u00fcchi objectives in alternating games on graphs is a central problem in computer-aided verification with a large number of applications. The long-standing best known upper bound for solving the problem is\n            <jats:italic>\u00d5<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            \u00b7\n            <jats:italic>m<\/jats:italic>\n            ), where\n            <jats:italic>n<\/jats:italic>\n            is the number of vertices and\n            <jats:italic>m<\/jats:italic>\n            is the number of edges in the graph. We are the first to break the\n            <jats:italic>\u00d5<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            \u00b7\n            <jats:italic>m<\/jats:italic>\n            ) boundary by presenting a new technique that reduces the running time to\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            ). This bound also leads to\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            )-time algorithms for computing the set of almost-sure winning vertices for B\u00fcchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of\n            <jats:italic>\u00d5<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            \u00b7\n            <jats:italic>m<\/jats:italic>\n            )), (2) in concurrent graph games with constant actions (improving an earlier bound of\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            )), and (3) in Markov decision processes (improving for\n            <jats:italic>m<\/jats:italic>\n            &gt;\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>4\/3<\/jats:sup>\n            an earlier bound of\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>m<\/jats:italic>\n            \u00b7 \u221a\n            <jats:italic>m<\/jats:italic>\n            )). We then show how to maintain the winning set for B\u00fcchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            ) amortized time per operation. Our algorithms are the first dynamic algorithms for this problem. We then consider another core graph theoretic problem in verification of probabilistic systems, namely computing the maximal end-component decomposition of a graph. We present two improved static algorithms for the maximal end-component decomposition problem. Our first algorithm is an\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>m<\/jats:italic>\n            \u00b7 \u221a\n            <jats:italic>m<\/jats:italic>\n            )-time algorithm, and our second algorithm is an\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            )-time algorithm which is obtained using the same technique as for alternating B\u00fcchi games. Thus, we obtain an\n            <jats:italic>O<\/jats:italic>\n            (min {m \u00b7 \u221a\n            <jats:italic>m<\/jats:italic>\n            ,\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            })-time algorithm improving the long-standing\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            \u00b7\n            <jats:italic>m<\/jats:italic>\n            ) time bound. Finally, we show how to maintain the maximal end-component decomposition of a graph under a sequence of edge insertions or a sequence of edge deletions in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            ) amortized time per edge deletion, and\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>m<\/jats:italic>\n            ) worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem.\n          <\/jats:p>","DOI":"10.1145\/2597631","type":"journal-article","created":{"date-parts":[[2014,5,27]],"date-time":"2014-05-27T12:56:59Z","timestamp":1401195419000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Efficient and Dynamic Algorithms for Alternating B\u00fcchi Games and Maximal End-Component Decomposition"],"prefix":"10.1145","volume":"61","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Monika","family":"Henzinger","sequence":"additional","affiliation":[{"name":"University of Vienna, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,6,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/963927.963928"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/320613.320614"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/646833.708042"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of DATE. 1188--1193","author":"Bloem R.","unstructured":"R. Bloem , S. J. Galler , B. Jobstmann , N. Piterman , A. Pnueli , and M. Weiglhofer . 2007. Interactive presentation: Automatic hardware synthesis from specifications: A case study . In Proceedings of DATE. 1188--1193 . R. Bloem, S. J. Galler, B. Jobstmann, N. Piterman, A. Pnueli, and M. Weiglhofer. 2007. Interactive presentation: Automatic hardware synthesis from specifications: A case study. In Proceedings of DATE. 1188--1193."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.10"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.39"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19600060105"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 1st International Congress on Logic, Methodology, and Philosophy of Science","author":"B\u00fcchi J.","year":"1962","unstructured":"J. B\u00fcchi . 1962 . On a decision method in restricted second-order arithmetic . In Proceedings of the 1st International Congress on Logic, Methodology, and Philosophy of Science 1960. E. Nagel, P. Suppes, and A. Tarski, Eds., Stanford University Press, 1--11. J. B\u00fcchi. 1962. On a decision method in restricted second-order arithmetic. In Proceedings of the 1st International Congress on Logic, Methodology, and Philosophy of Science 1960. E. Nagel, P. Suppes, and A. Tarski, Eds., Stanford University Press, 1--11."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1969-0280205-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of SODA'11","author":"Chatterjee K.","unstructured":"K. Chatterjee and M. Henzinger . 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification . In Proceedings of SODA'11 . SIAM. K. Chatterjee and M. Henzinger. 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In Proceedings of SODA'11. SIAM."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of SODA. ACM-SIAM.","author":"Chatterjee K.","unstructured":"K. Chatterjee and M. Henzinger . 2012. An O(n2) algorithm for alternating B\u00fcchi games . In Proceedings of SODA. ACM-SIAM. K. Chatterjee and M. Henzinger. 2012. An O(n2) algorithm for alternating B\u00fcchi games. In Proceedings of SODA. ACM-SIAM."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the Symposium on Games in Design and Verification (GDV).","author":"Chatterjee K.","unstructured":"K. Chatterjee , T. Henzinger , and N. Piterman . 2006. Algorithms for B\u00fcchi games . In Proceedings of the Symposium on Games in Design and Verification (GDV). K. Chatterjee, T. Henzinger, and N. Piterman. 2006. Algorithms for B\u00fcchi games. In Proceedings of the Symposium on Games in Design and Verification (GDV)."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763535"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03092-5_4"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_34"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45220-1_11"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of SODA'04","author":"Chatterjee K.","unstructured":"K. Chatterjee , M. Jurdzi\u0144ski , and T. Henzinger . 2004. Quantitative stochastic parity games . In Proceedings of SODA'04 . SIAM, 121--130. K. Chatterjee, M. Jurdzi\u0144ski, and T. Henzinger. 2004. Quantitative stochastic parity games. In Proceedings of SODA'04. SIAM, 121--130."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958116"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_11"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Congress of Mathematicians. Institut Mittag-Leffler, 23--35","author":"Church A.","year":"1962","unstructured":"A. Church . 1962 . Logic, arithmetic, and automata . In Proceedings of the International Congress of Mathematicians. Institut Mittag-Leffler, 23--35 . A. Church. 1962. Logic, arithmetic, and automata. In Proceedings of the International Congress of Mathematicians. Institut Mittag-Leffler, 23--35."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90048-K"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086265"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_28_1","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits","author":"Dill D.","unstructured":"D. Dill . 1989. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits . The MIT Press . D. Dill. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. The MIT Press."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:8)2008"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322235"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"J. Filar and K. Vrieze. 1997. Competitive Markov Decision Processes. Springer-Verlag.   J. Filar and K. Vrieze. 1997. Competitive Markov Decision Processes. Springer-Verlag.","DOI":"10.1007\/978-1-4612-4054-9"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Y. Godhal K. Chatterjee and T. A. Henzinger. 2011. Synthesis of AMBA AHB from formal specification: A case study. J. Softw. Tools Techn. Transfer.  Y. Godhal K. Chatterjee and T. A. Henzinger. 2011. Synthesis of AMBA AHB from formal specification: A case study. J. Softw. Tools Techn. Transfer.","DOI":"10.1007\/s10009-011-0207-9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00009268"},{"key":"e_1_2_1_35_1","volume-title":"Dynamic Programming and Markov Processes","author":"Howard H.","unstructured":"H. Howard . 1960. Dynamic Programming and Markov Processes . MIT Press . H. Howard. 1960. Dynamic Programming and Markov Processes. MIT Press."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90039-8"},{"key":"e_1_2_1_37_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of STACS'00","author":"Jurdzi\u0144ski M.","unstructured":"M. Jurdzi\u0144ski . 2000. Small progress measures for solving parity games . In Proceedings of STACS'00 . Lecture Notes in Computer Science , vol. 1770 , Springer , 290--301. M. Jurdzi\u0144ski. 2000. Small progress measures for solving parity games. In Proceedings of STACS'00. Lecture Notes in Computer Science, vol. 1770, Springer, 290--301."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737413"},{"key":"e_1_2_1_39_1","volume-title":"Classical Descriptive Set Theory","author":"Kechris A.","unstructured":"A. Kechris . 1995. Classical Descriptive Set Theory . Springer . A. Kechris. 1995. Classical Descriptive Set Theory. Springer."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/646337.688410"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1055686.1055689"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of LICS. 81--92","author":"Kupferman O.","unstructured":"O. Kupferman and M. Y. Vardi . 1998. Freedom, weakness, and determinism: From linear-time to branching-time . In Proceedings of LICS. 81--92 . O. Kupferman and M. Y. Vardi. 1998. Freedom, weakness, and determinism: From linear-time to branching-time. In Proceedings of LICS. 81--92."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the Workshop on Advances in Verification (WAVE'00)","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . 2000. Verifying randomized distributed algorithms with prism . In Proceedings of the Workshop on Advances in Verification (WAVE'00) . M. Kwiatkowska, G. Norman, and D. Parker. 2000. Verifying randomized distributed algorithms with prism. In Proceedings of the Workshop on Advances in Verification (WAVE'00)."},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of SODA. 1438--1445","author":"Lacki J.","year":"2011","unstructured":"J. Lacki . 2011 . Improved deterministic algorithms for decremental transitive closure and strongly connected components . In Proceedings of SODA. 1438--1445 . J. Lacki. 2011. Improved deterministic algorithms for decremental transitive closure and strongly connected components. In Proceedings of SODA. 1438--1445."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2459"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90036-D"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_24"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00008917"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_52_1","unstructured":"M. Stoelinga. 2002. Fun with FireWire: Experiments with verifying the IEEE 1394 root contention protocol. In Formal Aspects of Computing.  M. Stoelinga. 2002. Fun with FireWire: Experiments with verifying the IEEE 1394 root contention protocol. In Formal Aspects of Computing."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_54_1","volume-title":"Handbook of Formal Languages","author":"Thomas W.","unstructured":"W. Thomas . 1997. Languages , automata, and logic . In Handbook of Formal Languages , G. Rozenberg and A. Salomaa, Eds., Vol. 3 , Beyond Words, Springer , 389--455. W. Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Languages, G. Rozenberg and A. Salomaa, Eds., Vol. 3, Beyond Words, Springer, 389--455."},{"key":"e_1_2_1_55_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation","author":"Vardi M.","unstructured":"M. Vardi . 2007a. Automata-theoretic model checking revisited . In Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation . Lecture Notes in Computer Science , vol. 4349 , Springer , 137--150. M. Vardi. 2007a. Automata-theoretic model checking revisited. In Proceedings of the Symposium on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4349, Springer, 137--150."},{"key":"e_1_2_1_56_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science","author":"Vardi M.","unstructured":"M. Vardi . 2007b. The B\u00fcchi complementation saga . In Proceedings of the Symposium on Theoretical Aspects of Computer Science . Lecture Notes in Computer Science , vol. 4393 , Springer , 12--22. M. Vardi. 2007b. The B\u00fcchi complementation saga. In Proceedings of the Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 4393, Springer, 12--22."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2597631","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2597631","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:09:58Z","timestamp":1750234198000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2597631"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,5]]}},"alternative-id":["10.1145\/2597631"],"URL":"https:\/\/doi.org\/10.1145\/2597631","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5]]},"assertion":[{"value":"2012-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}