Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)

TL;DR

This paper introduces a tractable algorithm for complex probabilistic reachability questions in Markov decision processes, with significant performance improvements over existing solvers in specific cases.

Contribution

It presents a novel, efficient algorithm for relational reachability in probabilistic models, extending verification capabilities for security and randomized algorithms.

Findings

Algorithm outperforms general solvers on targeted benchmarks

Provides tractability results for certain reachability variations

Proves computational hardness for some problem variants

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.