Out of Control: Reducing Probabilistic Models by Control-State Elimination
share
We present a new, simple technique to reduce state space sizes in probabilistic model checking when the input model is defined in a programming formalism like the PRISM modeling language. Similar in spirit to traditional compiler optimizations that try to summarize instruction sequences into shorter ones, 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 probabilistic 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 various reduction techniques, our approach is property-directed. In many cases, it suffices to compute the reduced program only once to analyze it for many different parameter configurations - a rather common workflow in probabilistic model checking. Experiments demonstrate that our simple technique yields a state-space reduction of about one order of magnitude on practically relevant benchmarks.
READ FULL TEXT