2026-07-22T14:05:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14193 2024-03-06T10:53:43Z ddc:004 open_access

Faster Algorithms for Bounded Liveness in Graphs and Game Graphs Chatterjee, Krishnendu Henzinger, Monika Kale, Sagar Sudhir Svozil, Alexander Graphs Game Graphs Büchi 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Krishnendu Chatterjee and Monika Henzinger and Sagar Sudhir Kale and Alexander Svozil 2021 Is Part Of LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2021.124 urn:nbn:de:0030-drops-141930 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.124 eng https://creativecommons.org/licenses/by/4.0/legalcode