Disjunctive Reachability Queries in MDPs
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 , determine whether there is an infinite path that visits a vertex in at least once (i.e. you want to reach some vertex in ). Furthermore, given 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.
Parameters
- : number of vertices
- : number of edges
- : O(\min(n^2, m^{1.5}))
Filters
Computational Model
Randomization
Approximation
Algorithms Table
Insuffient Data to display table
Reductions Table
Displaying 2 of 2 reductions
Other relevant algorithms
Insuffient Data to display table