Disjunctive Reachability Queries in MDPs: Difference between revisions
(Created page with "{{DISPLAYTITLE:Disjunctive Reachability Queries in MDPs (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 Markov Decision Process (MDP), and the objective is reachability: given a set of target vertices $T\subseteq V$, determine whether there is an infinite path that visits a vertex in $T$ at least once (i.e. you want to reach...") |
No edit summary |
||
| (2 intermediate revisions by the same user not shown) | |||
| Line 18: | Line 18: | ||
== Parameters == | == Parameters == | ||
$n$: number of vertices | |||
m: number of edges | |||
$m$: number of edges | |||
MEC: O(\min(n^2, m^{1.5})) | |||
$MEC$: O(\min(n^2, m^{1.5})) | |||
== Table of Algorithms == | == Table of Algorithms == | ||
Currently no algorithms in our database for the given problem. | Currently no algorithms in our database for the given problem. | ||
== Reductions FROM Problem == | |||
{| class="wikitable sortable" style="text-align:center;" width="100%" | |||
! Problem !! Implication !! Year !! Citation !! Reduction | |||
|- | |||
| [[Triangle Detection]] || style="text-align:left;" | assume: Strong Triangle<br/>then: there is no combinatorial $O(n^{3-\epsilon})$ or $O((k \cdot n^{2})^{1-\epsilon})$ algorithm for any $\epsilon > {0}$ for target. The bounds holf for dense MDPs with $m=\Theta(n^{2})$ || 2016 || https://dl-acm-org.ezproxy.canberra.edu.au/doi/pdf/10.1145/2933575.2935304 || [[Reduction from Triangle Detection to Disjunctive Reachability Queries in MDPs|link]] | |||
|- | |||
| [[OV]] || style="text-align:left;" | assume: Strong Triangle<br/>then: there is no $O(m^{2-\epsilon})$ or $O((k \cdot m)^{1-\epsilon})$ algorithm, for any $\epsilon > {0}$ for target. || 2016 || https://dl-acm-org.ezproxy.canberra.edu.au/doi/pdf/10.1145/2933575.2935304 || [[Reduction from OV to Disjunctive Reachability Queries in MDPs|link]] | |||
|- | |||
|} | |||
Latest revision as of 09: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 Markov Decision Process (MDP), and the objective is reachability: given a set of target vertices $T\subseteq V$, determine whether there is an infinite path that visits a vertex in $T$ at least once (i.e. you want to reach some vertex in $T$).
Furthermore, given $k$ reachability objectives, the disjunctive reachability query question asks whether there is a strategy for player 1 to ensure that one of the reachability objectives is satisfied with probability 1.
Disjunctive queries do not coincide with disjunctive objectives on MDPs.
Related Problems
Generalizations: Reachability in MDPs
Related: 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, 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})$ algorithm for any $\epsilon > {0}$ for target. The bounds holf for dense MDPs with $m=\Theta(n^{2})$ |
2016 | https://dl-acm-org.ezproxy.canberra.edu.au/doi/pdf/10.1145/2933575.2935304 | link |
| OV | assume: Strong Triangle then: there is no $O(m^{2-\epsilon})$ or $O((k \cdot m)^{1-\epsilon})$ algorithm, for any $\epsilon > {0}$ for target. |
2016 | https://dl-acm-org.ezproxy.canberra.edu.au/doi/pdf/10.1145/2933575.2935304 | link |