Disjunctive Safety 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 safety: given a set of target vertices , determine whether there is an infinite path that does not visit any vertex in (i.e. you want to avoid all vertices in ). Furthermore, given safety objectives, the disjunctive safety query question asks whether there is a strategy for player 1 to ensure that one of the safety 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
Insuffient Data to display table
Other relevant algorithms
Insuffient Data to display table