Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour, Sebastian Junges
TL;DR
This paper addresses relational reachability in Markov decision processes, where the goal is to determine whether there exist schedulers that make multiple reachability probabilities satisfy inequalities, equalities (exact or approximate), or weighted sums. It develops a practical algorithm that reduces relational queries to optimal expected reward computations on goal unfoldings, using MEC-quotients to enable tractable linear-programming solutions and allowing approximate solutions with guaranteed bounds. The authors provide a comprehensive complexity landscape, proving PSPACE-hardness and EXPTIME membership in general, but identifying fixed-parameter tractable cases and PTIME fragments (e.g., absorbing targets or independent schedulers). A prototype implementation on Storm showcases substantial performance gains over state-of-the-art probabilistic hyperproperty solvers on the fragment it supports, highlighting the approach's scalability and practicality for security-relevant relational queries and beyond standard MOMC tasks.
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.