Disjunctive coBüchi Objectives: Difference between revisions
(Created page with "{{DISPLAYTITLE:Disjunctive coBüchi Objectives (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 coBüchi: given a set of target vertices $T\subseteq V$, determine whether or not there is a path that visits the set $T$ a finite amount of times. Furthermore, in the disjunctive problem, you a...") |
No edit summary |
||
| Line 14: | Line 14: | ||
== Parameters == | == Parameters == | ||
$n$: number of vertices | |||
$m$: number of edges | |||
$MEC$: O(\min(n^2, m^{1.5})) | |||
== Table of Algorithms == | == Table of Algorithms == | ||
Latest revision as of 08:28, 10 April 2023
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 coBüchi: given a set of target vertices $T\subseteq V$, determine whether or not there is a path that visits the set $T$ a finite amount of times.
Furthermore, in the disjunctive problem, you are given multiple coBüchi objectives (i.e. multiple target sets $T_i$) and you are to determine whether or not there is a path where at least one of the coBüchi objectives is satisfied (i.e. whether or not an infinite path visits any target set $T_i$ a finite 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, Generalized Büchi Games
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 |
|---|---|---|---|---|
| Triangle Detection | assume: Strong Triangle then: there is no combinatorial $O(n^{3-\epsilon})$ or $O((k\cdot n^{2})^{1-\epsilon})$-time algorithm for any $epsilon > {0}$ for generalized Büchi games. In particular, there is no such algorithm deciding whether the winning set is non-empty or deciding whether a specific vertex is in the winning set. |
2016 | https://arxiv.org/pdf/1607.05850.pdf | link |