Author(s):

Chatterjee, Krishnendu; Henzinger, Monika

Article Title: 
Efficient and dynamic algorithms for alternating Büchi games and maximal endcomponent decomposition

Affiliation 
IST Austria 
Abstract: 
The computation of the winning set for Büchi objectives in alternating games on graphs is a central problem in computeraided verification with a large number of applications. The longstanding 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 almostsure 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>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 endcomponent decomposition of a graph. We present two improved static algorithms for the maximal endcomponent 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 &lcu;m ⋅ √m,n2})time algorithm improving the longstanding O(n ⋅ m) time bound. Finally, we show how to maintain the maximal endcomponent 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) worstcase time per edge insertion. Again, our algorithms are the first dynamic algorithms for this problem.

Keywords: 
Graph games; Büchi objectives; Dynamic graph algorithms; Graph algorithms; Verification and synthesis

Journal Title:

Journal of the ACM

Volume: 
61

Issue 
3

ISSN:

00045411

Publisher:

ACM

Date Published:

20140501

Start Page: 
Article Number: 15

URL: 

DOI: 
10.1145/2597631

Notes: 
The research was supported by Austrian Science Fund (FWF) Grant No P 23499N23 on Modern Graph
Algorithmic Techniques in Formal Verification, Vienna Science and Technology Fund (WWTF) Grant ICT10
002, FWF NFN Grant No S11407N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft
faculty fellows award.
We thank anonymous reviewers for helpful comments that helped us to improve the presentation of this article.

Open access: 
yes (repository) 