Generalized Büchi Games (Model-Checking Problem)
Description
Given a model of a system and an objective, the model-checking problem asks whether the model satisfies the objective.
In this case, the model is a standard graph, and the objective is Büchi: given a set of target vertices $T\subseteq V$, determine whether or not there is a path that visits the set $T$ an infinite amount of times.
Furthermore, in the conjunctive problem, you are given multiple Büchi objectives (i.e. multiple target sets $T_i$) and you are to determine whether or not there is a path where all of the Büchi objectives are satisfied (i.e. whether or not an infinite path visits all target sets $T_i$ an infinite amount of times).
Related Problems
Related: Reachability in MDPs, Disjunctive Reachability Queries in MDPs, Conjunctive Reachability Queries in MDPs, Safety in MDPs, Disjunctive Safety Queries in MDPs, Conjunctive Safety Queries in MDPs, Safety in Graphs, Disjunctive Queries of Safety in Graphs, Disjunctive coBüchi Objectives
Parameters
$n$: number of vertices
$m$: number of edges
$MEC$: O(\min(n^2, m^{1.5}))
Table of Algorithms
Currently no algorithms in our database for the given problem.
Reductions FROM Problem
| Problem | Implication | Year | Citation | Reduction |
|---|---|---|---|---|
| OV | assume: OVH then: there is no $O(m^{2-\epsilon})$ or $O(\min_{1 \leq i \leq k} b_i \cdot (k \cdot m)^{1-\epsilon})$-time algorithm (for any $\epsilon > {0}$ for generalized Büchi games. In particular there is no such algorithm for deciding whether the winning set is non-empty or deciding whether a specifc vertex is in the winning set. |
2016 | https://arxiv.org/pdf/1607.05850.pdf | link |