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

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})$
then: there is no $O(m^{2-\epsilon})$ or $O((k \cdot m)^{1-\epsilon})$ algorithm, for any $\epsilon > {0}$ for target.