Finite-Horizon Bisimulation Minimisation for Probabilistic Systems

Nishanthan Kamaleson, David Parker, Jonathan Rowe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)
248 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationModel Checking Software
Subtitle of host publication23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
PublisherSpringer
Pages147-164
Number of pages18
ISBN (Electronic)978-3-319-32582-8
ISBN (Print)978-3-319-32581-1
DOIs
Publication statusPublished - 8 Apr 2016
Event23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016 - Eindhoven, Netherlands
Duration: 7 Apr 20168 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9641

Conference

Conference23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016
Country/TerritoryNetherlands
CityEindhoven
Period7/04/168/04/16

Fingerprint

Dive into the research topics of 'Finite-Horizon Bisimulation Minimisation for Probabilistic Systems'. Together they form a unique fingerprint.

Cite this