Safety 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 safety: given a set of target vertices $T\subseteq V$, determine whether there is an infinite path that does not visit any vertex in $T$ (i.e. you want to avoid all vertices in $T$).

Related Problems

Generalizations: Safety in Graphs

Subproblem: Disjunctive Safety Queries in MDPs, Conjunctive Safety Queries in MDPs

Related: Reachability in MDPs, Disjunctive Reachability Queries in MDPs, Conjunctive Reachability Queries in MDPs, Conjunctive Safety Queries in MDPs, 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.