Finite-Horizon Bisimulation Minimisation for Probabilistic Systems

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

Standard

Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. / Kamaleson, Nishanthan; Parker, David; Rowe, Jonathan.

Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer, 2016. p. 147-164 (Lecture Notes in Computer Science; Vol. 9641).

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

Harvard

Kamaleson, N, Parker, D & Rowe, J 2016, Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. in Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9641, Springer, pp. 147-164, 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, Netherlands, 7/04/16. https://doi.org/10.1007/978-3-319-32582-8_10

APA

Kamaleson, N., Parker, D., & Rowe, J. (2016). Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. In Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings (pp. 147-164). (Lecture Notes in Computer Science; Vol. 9641). Springer. https://doi.org/10.1007/978-3-319-32582-8_10

Vancouver

Kamaleson N, Parker D, Rowe J. Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. In Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer. 2016. p. 147-164. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-32582-8_10

Author

Kamaleson, Nishanthan ; Parker, David ; Rowe, Jonathan. / Finite-Horizon Bisimulation Minimisation for Probabilistic Systems. Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer, 2016. pp. 147-164 (Lecture Notes in Computer Science).

Bibtex

@inproceedings{f36fa1ac6fd64ccd8c3841dead5c9f06,
title = "Finite-Horizon Bisimulation Minimisation for Probabilistic Systems",
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{\textquoteright}s existing efficient implementations of probabilistic verification.",
author = "Nishanthan Kamaleson and David Parker and Jonathan Rowe",
year = "2016",
month = apr,
day = "8",
doi = "10.1007/978-3-319-32582-8_10",
language = "English",
isbn = "978-3-319-32581-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "147--164",
booktitle = "Model Checking Software",
note = "23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016 ; Conference date: 07-04-2016 Through 08-04-2016",

}

RIS

TY - GEN

T1 - Finite-Horizon Bisimulation Minimisation for Probabilistic Systems

AU - Kamaleson, Nishanthan

AU - Parker, David

AU - Rowe, Jonathan

PY - 2016/4/8

Y1 - 2016/4/8

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-32582-8_10

DO - 10.1007/978-3-319-32582-8_10

M3 - Conference contribution

SN - 978-3-319-32581-1

T3 - Lecture Notes in Computer Science

SP - 147

EP - 164

BT - Model Checking Software

PB - Springer

T2 - 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016

Y2 - 7 April 2016 through 8 April 2016

ER -