Out of Control: Reducing Probabilistic Models by Control-State Elimination

TL;DR

This paper introduces a novel, automatic program-level reduction technique for probabilistic models that significantly decreases state space size, enhancing the efficiency of model checking by summarizing control-flow graph behaviors.

Contribution

The authors propose a new property-directed reduction method that operates at the program level, reducing control states in Markov models without relying on explicit-state minimization techniques.

Findings

Achieves up to 80% state-space reduction on benchmarks

Supports property-directed and parameterized models

Enables more efficient probabilistic model checking

Abstract

State-of-the-art probabilistic model checkers perform verification on explicit-state Markov models defined in a high-level programming formalism like the PRISM modeling language. Typically, the low-level models resulting from such program-like specifications exhibit lots of structure such as repeating subpatterns. Established techniques like probabilistic bisimulation minimization are able to exploit these structures; however, they operate directly on the explicit-state model. On the other hand, methods for reducing structured state spaces by reasoning about the high-level program have not been investigated that much. In this paper, we present a new, simple, and fully automatic program-level technique to reduce the underlying Markov model. Our approach aims at computing the summary behavior of adjacent locations in the program's control-flow graph, thereby obtaining a program with fewer "control states". This reduction is immediately reflected in the program's operational semantics, enabling more efficient model checking. A key insight is that in principle, each (combination of) program variable(s) with finite domain can play the role of the program counter that defines the flow structure. Unlike most other reduction techniques, our approach is property-directed and naturally supports unspecified model parameters. Experiments demonstrate that our simple method yields state-space reductions of up to 80% on practically relevant benchmarks.