Conjunctive Safety Queries in MDPs: Difference between revisions

From Algorithm Wiki
Jump to navigation Jump to search
(Created page with "{{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...")
 
No edit summary
 
(One intermediate revision by the same user not shown)
Line 18: Line 18:
== Parameters ==  
== Parameters ==  


<pre>n: number of vertices
$n$: number of vertices
m: number of edges
 
k: number of objectives
$m$: number of edges
MEC: O(\min(n^2, m^{1.5}))</pre>
 
$MEC$: O(\min(n^2, m^{1.5}))


== Table of Algorithms ==  
== Table of Algorithms ==  


Currently no algorithms in our database for the given problem.
Currently no algorithms in our database for the given problem.

Latest revision as of 08:28, 10 April 2023

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

$MEC$: O(\min(n^2, m^{1.5}))

Table of Algorithms

Currently no algorithms in our database for the given problem.