View source for Conjunctive Safety Queries in MDPs

{{DISPLAYTITLE:Conjunctive Safety 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 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$).

Furthermore, given $k$ safety objectives, the conjunctive safety query question asks whether there is a strategy for player 1 to ensure that all the safety objectives are satisfied with probability 1.

Conjunctive queries coincide with conjunctive objectives on graphs and MDPs.

== Related Problems == 

Generalizations: [[Safety in MDPs]]

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