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 TVT\subseteq V, determine whether there is an infinite path that visits a vertex in TT at least once (i.e. you want to reach some vertex in TT). Furthermore, given kk 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

  • nn: number of vertices
  • mm: number of edges
  • MECMEC: O(\min(n^2, m^{1.5}))

Insufficient data to display graph

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