Conditionally Optimal Algorithms for Generalized B\"uchi Games

DOI10.4230/LIPICS.MFCS.2016.25MaRDI QIDQ4608584zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Wolfgang Dvořák, Veronika Loitzenbauer, Monika R. Henzinger

Publication date 21 March 2018

Full work available at URL https://arxiv.org/abs/1607.05850

zbMATH Keywords

graph algorithmsgraph gamescomputer-aided verificationconditional lower bounds\(\mathrm{GR}(1)\) objectivegeneralized Büchi objective

Mathematics Subject Classification ID

Graph algorithms (graph-theoretic aspects) (05C85) Graph theory (including graph drawing) in computer science (68R10) Analysis of algorithms (68W40) Games involving graphs (91A43)

Abstract: Games on graphs provide the appropriate framework to study several central problems in computer science, such as the verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or B"uchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized B"uchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized B"uchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with $n$ vertices, $m$ edges, and generalized B"uchi objectives with $k$ conjunctions. First, we present an algorithm with running time $O(kcdot{n}^2)$, improving the previously known $O(kcdotncdotm)$ and $O(k^{2}cdot{n}^2)$ worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with $k_1$ conjunctions in the antecedent and $k_2$ conjunctions in the consequent, and present an $O(k_{1}cdot{k}_{2}cdot{n}^{2.5})$-time algorithm, improving the previously known $O(k_{1}cdot{k}_{2}cdotncdotm)$-time algorithm for $m>n^{1.5}$.

Recommendations

• Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
• Algorithms for generalized potential games with mixed-integer variables
• Necessary and sufficient conditions for optimality in constrained general sum stochastic games
• An \(O(n^2)\) time algorithm for alternating Büchi games
• Exact algorithms for solving stochastic games
• Decomposition algorithms for generalized potential games
• Optimization and dynamical systems algorithms for finding equilibria of stochastic games
• Efficient Algorithms for Constant Well Supported Approximate Equilibria in Bimatrix Games
• scientific article; zbMATH DE number 2143159
• An algorithm for payoff space in \(C^1\) parametric games

Cited in

(9)

• Model and objective separation with conditional lower bounds: disjunction is harder than conjunction
• Improved algorithms for one-pair and \(k\)-pair Streett objectives
• Fine-grained complexity lower bounds for problems in computer aided verification
• Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition
• An \(O(n^2)\) time algorithm for alternating Büchi games
• Parameterized complexity of games with monotonically ordered \(\omega\)-regular objectives
• Multi-buffer simulations for trace language inclusion
• Algorithms and conditional lower bounds for planning problems
• Improved algorithms for parity and Streett objectives

This page was built for publication: Conditionally Optimal Algorithms for Generalized B\"uchi Games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4608584)