HomeNewsCase StudiesPeoplePublications
[DKP13] C. Dehnert, J.-P. Katoen and D. Parker. SMT-Based Bisimulation Minimisation of Markov Models. In Proc. 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'13), volume 7737 of LNCS, pages 28-47, Springer. January 2013. [pdf] [bib]
Downloads:  pdf pdf (417 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. Probabilistic model checking is an increasingly widely used formal verification technique. However, its dependence on computationally expensive numerical operations makes it particularly susceptible to the state-space explosion problem. Among other abstraction techniques, bisimulation minimisation has proven to shorten computation times significantly, but, usually, the full state space needs to be built prior to minimisation. We present a novel approach that leverages satisfiability solvers to extract the minimised system from a high-level description directly. A prototypical implementation in the framework of the probabilistic model checker PRISM provides encouraging experimental results.