article published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Monika H Henzinger author 540c9bbd-f2de-11ec-812d-d04a5be856300000-0002-5008-6530 KrCh department Modern Graph Algorithmic Techniques in Formal Verification project Efficient Algorithms for Computer Aided Verification project Game Theory project Quantitative Graph Games: Theory and Applications project Microsoft Research Faculty Fellowship project The computation of the winning set for Büchi 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 ⋅ m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the Õ(n ⋅ m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2)-time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of Õ(n ⋅ m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m&gt;n4/3 an earlier bound of O(m ⋅ √m)). We then show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(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 O(m ⋅ √m)-time algorithm, and our second algorithm is an O(n2)-time algorithm which is obtained using the same technique as for alternating Büchi games. Thus, we obtain an O(min &amp;lcu;m ⋅ √m,n2})-time algorithm improving the long-standing O(n ⋅ m) 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 O(n) amortized time per edge deletion, and O(m) worst-case time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem. ACM2014 eng 00033720140000110.1145/2597631 613 https://research-explorer.ista.ac.at/record/3165 Chatterjee K, Henzinger M. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. <i>Journal of the ACM</i>. 2014;61(3). doi:<a href="https://doi.org/10.1145/2597631">10.1145/2597631</a> Chatterjee K, Henzinger M. 2014. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. Journal of the ACM. 61(3), a15. K. Chatterjee and M. Henzinger, “Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition,” <i>Journal of the ACM</i>, vol. 61, no. 3. ACM, 2014. K. Chatterjee, M. Henzinger, Journal of the ACM 61 (2014). Chatterjee, K., &#38; Henzinger, M. (2014). Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/2597631">https://doi.org/10.1145/2597631</a> Chatterjee, Krishnendu, and Monika Henzinger. “Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition.” <i>Journal of the ACM</i>. ACM, 2014. <a href="https://doi.org/10.1145/2597631">https://doi.org/10.1145/2597631</a>. Chatterjee, Krishnendu, and Monika Henzinger. “Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition.” <i>Journal of the ACM</i>, vol. 61, no. 3, a15, ACM, 2014, doi:<a href="https://doi.org/10.1145/2597631">10.1145/2597631</a>. 21412018-12-11T11:55:57Z2025-09-29T11:45:13Z