XPL: An extended probabilistic logic for probabilistic transition systems

TL;DR

XPL extends generalized probabilistic logic to handle nondeterminism in Markov decision processes, enabling a unified framework for analyzing various probabilistic systems, with a decidable subclass called separable XPL.

Contribution

The paper introduces XPL, an extended probabilistic logic that captures nondeterminism in MDPs, and defines separable XPL for decidable model checking of complex probabilistic systems.

Findings

XPL can express multiple probabilistic verification problems.

Model checking in XPL is undecidable in general.

Separable XPL offers a decidable fragment for key problems.

Abstract

Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of reactive probabilistic systems. We explore XPL, an extension to GPL allowing the semantics of nondeterminism present in Markov decision processes (MDPs). XPL is expressive enough that a number of independently studied problems--- such as termination of Recursive MDPs (RMDPs), PCTL* model checking of MDPs, and reachability for Branching MDPs--- can all be cast as model checking over XPL. Termination of multi-exit RMDPs is undecidable; thus, model checking in XPL is undecidable in general. We define a subclass, called separable XPL, for which model checking is decidable. Decidable problems such as termination of 1-exit RMDPs, PCTL* model checking of MDPs, and reachability for Branching MDPs can be reduced to model checking separable XPL. Thus, XPL forms a uniform framework for studying problems involving systems with non-deterministic and probabilistic behaviors, while separable XPL provides a way to solve decidable fragments of these problems.