Projects per year
Abstract
We give polynomial time algorithms for quantitative (and qualitative) reachability analysis for Branching Markov Decision Processes (BMDPs). Specically, given a BMDP, and given an initial population, where the objective of the controller is to maximize (or minimize) the probability of eventually reaching a population that contains an object of a desired (or undesired) type, we give algorithms for approximating the supremum (inmum) reachability probability, within desired precision > 0, in time polynomial in the encoding size of the BMDP and in log(1=). We furthermore give Ptime algorithms for computing optimal strategies for both maximization and minimization of reachability probabilities. We also give Ptime algorithms for all associated qualitative analysis problems, namely: deciding whether the optimal (supremum or inmum) reachability probabilities are 0 or 1. Prior to this paper, approximation of optimal reachability probabilities for BMDPs was not even known to be decidable. Our algorithms exploit the following basic fact: we show that for any BMDP, its maximum (minimum) nonreachability probabilities are given by the greatest xed point (GFP) solution g 2 [0; 1]n of a corresponding monotone max (min) Probabilistic Polynomial System of equations (max/minPPS), x = P(x), which are the Bellman optimality equations for a BMDP with nonreachability objectives. We show how to compute the GFP of max/minPPSs to desired precision in Ptime. We also study more general branching simple stochastic games (BSSGs) with (non)reachability objectives. We show that: (1) the value of these games is captured by the GFP, g, of a corresponding maxminPPS, x = P(x); (2) the quantitative problem of approximating the value is in TFNP; and (3) the qualitative problems associated with the value are all solvable in Ptime.
Original language  English 

Pages (fromto)  355382 
Number of pages  28 
Journal  Information and Computation 
Volume  261 
Issue number  2 
Early online date  8 Feb 2018 
DOIs  
Publication status  Published  Aug 2018 
Fingerprint
Dive into the research topics of 'Greatest Fixed Points of Probabilistic Min/Max Polynomial Equations, and Reachability for Branching Markov Decision Processes'. Together they form a unique fingerprint.Projects
 1 Finished

Efficient algorithms for verification of recursive probabilistic system
30/03/13 → 29/03/15
Project: Research
Profiles

Kousha Etessami
 School of Informatics  Personal Chair in Algorithms, Games, Logic and Complexity
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active