×

zbMATH — the first resource for mathematics

SMT-based bisimulation minimisation of Markov models. (English) Zbl 1426.68168
Giacobazzi, Roberto (ed.) et al., Verification, model checking, and abstract interpretation. 14th international conference, VMCAI 2013, Rome, Italy, January 20–22, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7737, 28-47 (2013).
Summary: 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.
For the entire collection see [Zbl 1298.68027].
Reviewer: Reviewer (Berlin)

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
60J20 Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Software:
CEGAR; PRISM; PVS; SIGREF
PDF BibTeX XML Cite
Full Text: DOI