---
res:
bibo_abstract:
- Games on graphs provide the appropriate framework to study several central problems
in computer science, such as verification and synthesis of reactive systems. One
of the most basic objectives for games on graphs is the liveness (or Büchi) objective
that given a target set of vertices requires that some vertex in the target set
is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction
of liveness objectives), and implications between two generalized Büchi 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üchi objectives with k conjunctions. First,
we present an algorithm with running time O(k*n^2), improving the previously known
O(k*n*m) and O(k^2*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 k_2 n^{2.5})-time
algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m
> n^{1.5}. @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: Wolfgang
foaf_name: Dvorák, Wolfgang
foaf_surname: Dvorák
- foaf_Person:
foaf_givenName: Monika
foaf_name: Henzinger, Monika
foaf_surname: Henzinger
- foaf_Person:
foaf_givenName: Veronika
foaf_name: Loitzenbauer, Veronika
foaf_surname: Loitzenbauer
bibo_doi: 10.4230/LIPIcs.MFCS.2016.25
bibo_volume: 58
dct_date: 2016^xs_gYear
dct_language: eng
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Conditionally optimal algorithms for generalized Büchi Games@
...