Bisimulation minimisation mostly speeds up probabilistic model checking

Joost P. Katoen, J.P. Katoen, T. Kemna, I.S. Zapreev, D.N. Jansen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

77 Citations (Scopus)

Abstract

This paper studies the effect of bisimulation minimisation in model checking of monolithic discrete-time and continuous-time Markov chains as well as variants thereof with rewards. Our results show that--as for traditional model checking--enormous state space reductions (up to logarithmic savings) may be obtained. In contrast to traditional model checking, in many cases, the verification time of the original Markov chain exceeds the quotienting time plus the verification time of the quotient. We consider probabilistic bisimulation as well as versions thereof that are tailored to the property be checked.
Original languageUndefined
Title of host publicationTools and algorithms for the construction and analysis of systems
EditorsO. Grumberg, M. Huth
Place of PublicationBerlin
PublisherSpringer
Pages87-101
Number of pages15
ISBN (Print)978-3-540-71208-4
DOIs
Publication statusPublished - 2007

Publication series

NameLecture notes in computer science
PublisherSpringer
Number2
Volume4424

Keywords

  • EWI-9651
  • IR-63995
  • METIS-241575

Cite this

Katoen, J. P., Katoen, J. P., Kemna, T., Zapreev, I. S., & Jansen, D. N. (2007). Bisimulation minimisation mostly speeds up probabilistic model checking. In O. Grumberg, & M. Huth (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 87-101). [10.1007/978-3-540-71209-1_9] (Lecture notes in computer science; Vol. 4424, No. 2). Berlin: Springer. https://doi.org/10.1007/978-3-540-71209-1_9
Katoen, Joost P. ; Katoen, J.P. ; Kemna, T. ; Zapreev, I.S. ; Jansen, D.N. / Bisimulation minimisation mostly speeds up probabilistic model checking. Tools and algorithms for the construction and analysis of systems. editor / O. Grumberg ; M. Huth. Berlin : Springer, 2007. pp. 87-101 (Lecture notes in computer science; 2).
@inproceedings{7515699c9f08400b95876e9ac0ac088b,
title = "Bisimulation minimisation mostly speeds up probabilistic model checking",
abstract = "This paper studies the effect of bisimulation minimisation in model checking of monolithic discrete-time and continuous-time Markov chains as well as variants thereof with rewards. Our results show that--as for traditional model checking--enormous state space reductions (up to logarithmic savings) may be obtained. In contrast to traditional model checking, in many cases, the verification time of the original Markov chain exceeds the quotienting time plus the verification time of the quotient. We consider probabilistic bisimulation as well as versions thereof that are tailored to the property be checked.",
keywords = "EWI-9651, IR-63995, METIS-241575",
author = "Katoen, {Joost P.} and J.P. Katoen and T. Kemna and I.S. Zapreev and D.N. Jansen",
note = "10.1007/978-3-540-71209-1_9",
year = "2007",
doi = "10.1007/978-3-540-71209-1_9",
language = "Undefined",
isbn = "978-3-540-71208-4",
series = "Lecture notes in computer science",
publisher = "Springer",
number = "2",
pages = "87--101",
editor = "O. Grumberg and M. Huth",
booktitle = "Tools and algorithms for the construction and analysis of systems",

}

Katoen, JP, Katoen, JP, Kemna, T, Zapreev, IS & Jansen, DN 2007, Bisimulation minimisation mostly speeds up probabilistic model checking. in O Grumberg & M Huth (eds), Tools and algorithms for the construction and analysis of systems., 10.1007/978-3-540-71209-1_9, Lecture notes in computer science, no. 2, vol. 4424, Springer, Berlin, pp. 87-101. https://doi.org/10.1007/978-3-540-71209-1_9

Bisimulation minimisation mostly speeds up probabilistic model checking. / Katoen, Joost P.; Katoen, J.P.; Kemna, T.; Zapreev, I.S.; Jansen, D.N.

Tools and algorithms for the construction and analysis of systems. ed. / O. Grumberg; M. Huth. Berlin : Springer, 2007. p. 87-101 10.1007/978-3-540-71209-1_9 (Lecture notes in computer science; Vol. 4424, No. 2).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Bisimulation minimisation mostly speeds up probabilistic model checking

AU - Katoen, Joost P.

AU - Katoen, J.P.

AU - Kemna, T.

AU - Zapreev, I.S.

AU - Jansen, D.N.

N1 - 10.1007/978-3-540-71209-1_9

PY - 2007

Y1 - 2007

N2 - This paper studies the effect of bisimulation minimisation in model checking of monolithic discrete-time and continuous-time Markov chains as well as variants thereof with rewards. Our results show that--as for traditional model checking--enormous state space reductions (up to logarithmic savings) may be obtained. In contrast to traditional model checking, in many cases, the verification time of the original Markov chain exceeds the quotienting time plus the verification time of the quotient. We consider probabilistic bisimulation as well as versions thereof that are tailored to the property be checked.

AB - This paper studies the effect of bisimulation minimisation in model checking of monolithic discrete-time and continuous-time Markov chains as well as variants thereof with rewards. Our results show that--as for traditional model checking--enormous state space reductions (up to logarithmic savings) may be obtained. In contrast to traditional model checking, in many cases, the verification time of the original Markov chain exceeds the quotienting time plus the verification time of the quotient. We consider probabilistic bisimulation as well as versions thereof that are tailored to the property be checked.

KW - EWI-9651

KW - IR-63995

KW - METIS-241575

U2 - 10.1007/978-3-540-71209-1_9

DO - 10.1007/978-3-540-71209-1_9

M3 - Conference contribution

SN - 978-3-540-71208-4

T3 - Lecture notes in computer science

SP - 87

EP - 101

BT - Tools and algorithms for the construction and analysis of systems

A2 - Grumberg, O.

A2 - Huth, M.

PB - Springer

CY - Berlin

ER -

Katoen JP, Katoen JP, Kemna T, Zapreev IS, Jansen DN. Bisimulation minimisation mostly speeds up probabilistic model checking. In Grumberg O, Huth M, editors, Tools and algorithms for the construction and analysis of systems. Berlin: Springer. 2007. p. 87-101. 10.1007/978-3-540-71209-1_9. (Lecture notes in computer science; 2). https://doi.org/10.1007/978-3-540-71209-1_9