Efficient Probabilistic Model Checking for Relational Reachability

Lecture notes in computer science, pp. 127–147

Abstract

Abstract Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability properties, such as: Is there a scheduler resolving the nondeterminism such that the probability to reach an error state is above a threshold? We consider an understudied extension that relates different reachability probabilities, such as: Is there a scheduler such that two sets of states are reached with different probabilities? These questions appear naturally in the design of randomized algorithms and in various security applications. We provide a tractable algorithm for many variations of this problem, while proving computational hardness of some others. An implementation of our algorithm beats solvers for more general probabilistic hyperlogics by orders of magnitude, on the subset of their benchmarks that are within our fragment.

Authors 5

1. Lina Gerlach Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Tobias Winkler Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Erika Ábrahám Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Borzoo Bonakdarpour

   Michigan State University

   Affiliation as printed

   Michigan State University, East Lansing, MI, USA

5. Sebastian Junges corresponding

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University, Nijmegen, The Netherlands