---
_id: '2141'
abstract:
- lang: eng
  text: 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>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 &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.
article_number: a15
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
citation:
  ama: 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>
  apa: 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>
  chicago: 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>.
  ieee: 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.
  ista: 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.
  mla: 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>.
  short: K. Chatterjee, M. Henzinger, Journal of the ACM 61 (2014).
date_created: 2018-12-11T11:55:57Z
date_published: 2014-05-01T00:00:00Z
date_updated: 2025-09-29T11:45:13Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2597631
ec_funded: 1
external_id:
  isi:
  - '000337201400001'
intvolume: '        61'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://eprints.cs.univie.ac.at/3933/
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '4883'
quality_controlled: '1'
related_material:
  record:
  - id: '3165'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Efficient and dynamic algorithms for alternating Büchi games and maximal end-component
  decomposition
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 61
year: '2014'
...