Out of Control: Reducing Probabilistic Models by Control-State Elimination
Most 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 and symbolic model checking 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 technique yields state-space reductions of up to 80% on practically relevant benchmarks, and by orders of magnitude on selected examples.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 11:50
|Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson|
|STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model CheckingRemote|
|EPMC Gets Knowledge in Multi-Agent SystemsRemote|
Chen Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Ernst Moritz Hahn University of Twente, Yong Li Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Meng Sun Peking University, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences