Generalized Büchi Games (Model-Checking Problem)

From Algorithm Wiki
Jump to navigation Jump to search


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


$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 link