Conjunctive 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 conjunctive reachability query question asks whether there is a strategy for player 1 to ensure that all the reachability objectives are satisfied with probability 1.
Conjunctive queries coincide with conjunctive objectives on graphs and MDPs.
Related Problems
Generalizations: Reachability in MDPs
Related: Disjunctive 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
k: number of objectives
MEC: O(\min(n^2, m^{1.5}))
Table of Algorithms
Currently no algorithms in our database for the given problem.