Kavli Affiliate: Johannes Lehmann
| First 5 Authors: Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen, ,
| Summary:
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.
| Search Query: ArXiv Query: search_query=au:”Johannes Lehmann”&id_list=&start=0&max_results=3