Finite-Horizon Bisimulation Minimisation for Probabilistic Systems
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Authors
Colleges, School and Institutes
Abstract
We present model reduction techniques to improve the efficiency and scalability of verifying probabilistic systems over a finite time horizon. We propose a finite-horizon variant of probabilistic bisimulation for discrete-time Markov chains, which preserves a bounded fragment of the temporal logic PCTL. In addition to a standard partitionrefinement based minimisation algorithm, we present on-the-fly finite-horizon minimisation techniques, which are based on a backwards traversal of the Markov chain, directly from a high-level model description. We investigate both symbolic and explicit-state implementations, using SMT solvers and hash functions, respectively, and implement them in the PRISM model checker. We show that finite-horizon reduction can provide significant reductions in model size, in some cases outperforming PRISM’s existing efficient implementations of probabilistic verification.
Details
Original language | English |
---|---|
Title of host publication | Model Checking Software |
Subtitle of host publication | 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings |
Publication status | Published - 8 Apr 2016 |
Event | 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016 - Eindhoven, Netherlands Duration: 7 Apr 2016 → 8 Apr 2016 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 9641 |
Conference
Conference | 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016 |
---|---|
Country | Netherlands |
City | Eindhoven |
Period | 7/04/16 → 8/04/16 |