@inproceedings{10054,
  abstract     = {Graphs and games on graphs are fundamental models for the analysis of reactive systems, in particular, for model-checking and the synthesis of reactive systems. The class of ω-regular languages provides a robust specification formalism for the desired properties of reactive systems. In the classical infinitary formulation of the liveness part of an ω-regular specification, a "good" event must happen eventually without any bound between the good events. A stronger notion of liveness is bounded liveness, which requires that good events happen within d transitions. Given a graph or a game graph with n vertices, m edges, and a bounded liveness objective, the previous best-known algorithmic bounds are as follows: (i) O(dm) for graphs, which in the worst-case is O(n³); and (ii) O(n² d²) for games on graphs. Our main contributions improve these long-standing algorithmic bounds. For graphs we present: (i) a randomized algorithm with one-sided error with running time O(n^{2.5} log n) for the bounded liveness objectives; and (ii) a deterministic linear-time algorithm for the complement of bounded liveness objectives. For games on graphs, we present an O(n² d) time algorithm for the bounded liveness objectives.},
  author       = {Chatterjee, Krishnendu and Henzinger, Monika H and Kale, Sagar Sudhir and Svozil, Alexander},
  booktitle    = {48th International Colloquium on Automata, Languages, and Programming},
  isbn         = {978-3-95977-195-5},
  issn         = {1868-8969},
  location     = {Glasgow, Scotland},
  publisher    = {Schloss Dagstuhl - Leibniz Zentrum für Informatik},
  title        = {{Faster algorithms for bounded liveness in graphs and game graphs}},
  doi          = {10.4230/LIPIcs.ICALP.2021.124},
  volume       = {198},
  year         = {2021},
}