---
res:
bibo_abstract:
- Computing 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(n 2). This bound also leads to O(n 2) 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(n 3)), and (3) in Markov decision processes (improving for m > n
4/3 an earlier bound of O(min(m 1.5, m·n 2/3)). We also show that the same technique
can be used to compute the maximal end-component decomposition of a graph in time
O(n 2), which is an improvement over earlier bounds for m > n 4/3. Finally,
we 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. This is the first dynamic algorithm for this problem.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Monika
foaf_name: Henzinger, Monika
foaf_surname: Henzinger
bibo_doi: 10.1137/1.9781611973099.109
dct_date: 2012^xs_gYear
dct_language: eng
dct_publisher: SIAM@
dct_title: An O(n2) time algorithm for alternating Büchi games@
...