Bisimulation minimisation mostly speeds up probabilistic model checking

Joost-Pieter Katoen; Tim Kemna; Ivan Zapreev; David N. Jansen

doi:10.1007/978-3-540-71209-1_9

Bisimulation minimisation mostly speeds up probabilistic model checking

Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, David N. Jansen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

90 Citations (Scopus)

20 Downloads (Pure)

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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings
Editors	Orna Grumberg, Michael Huth
Place of Publication	Berlin
Publisher	Springer
Pages	87-101
Number of pages	15
ISBN (Electronic)	978-3-540-71209-1
ISBN (Print)	978-3-540-71208-4
DOIs	https://doi.org/10.1007/978-3-540-71209-1_9
Publication status	Published - 2007
Event	13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 - Braga, Portugal Duration: 24 Mar 2007 → 1 Apr 2007 Conference number: 13

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4424
ISSN (Print)	0302-9743

Name	Theoretical Computer Science and General Issues
Publisher	Springer
ISSN (Print)	2512-2010
ISSN (Electronic)	2512-2029

Conference

Conference	13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007
Abbreviated title	TACAS
Country/Territory	Portugal
City	Braga
Period	24/03/07 → 1/04/07

Access to Document

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

ArticleFinal published version, 574 KBLicence: Taverne

Cite this

Katoen, J.-P., Kemna, T., Zapreev, I., & 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: 13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings (pp. 87-101). (Lecture Notes in Computer Science; Vol. 4424), (Theoretical Computer Science and General Issues). Springer. https://doi.org/10.1007/978-3-540-71209-1_9

Katoen, Joost-Pieter ; Kemna, Tim ; Zapreev, Ivan et al. / Bisimulation minimisation mostly speeds up probabilistic model checking. Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. editor / Orna Grumberg ; Michael Huth. Berlin : Springer, 2007. pp. 87-101 (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues).

@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.",

author = "Joost-Pieter Katoen and Tim Kemna and Ivan Zapreev and Jansen, {David N.}",

year = "2007",

doi = "10.1007/978-3-540-71209-1_9",

language = "English",

isbn = "978-3-540-71208-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "87--101",

editor = "Orna Grumberg and Michael Huth",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007, TACAS ; Conference date: 24-03-2007 Through 01-04-2007",

}

Katoen, J-P, Kemna, T, Zapreev, I & 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: 13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4424, Theoretical Computer Science and General Issues, Springer, Berlin, pp. 87-101, 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007, Braga, Portugal, 24/03/07. https://doi.org/10.1007/978-3-540-71209-1_9

Bisimulation minimisation mostly speeds up probabilistic model checking. / Katoen, Joost-Pieter; Kemna, Tim; Zapreev, Ivan et al.
Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. ed. / Orna Grumberg; Michael Huth. Berlin: Springer, 2007. p. 87-101 (Lecture Notes in Computer Science; Vol. 4424), (Theoretical Computer Science and General Issues).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Bisimulation minimisation mostly speeds up probabilistic model checking

AU - Katoen, Joost-Pieter

AU - Kemna, Tim

AU - Zapreev, Ivan

AU - Jansen, David N.

N1 - Conference code: 13

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.

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, Orna

A2 - Huth, Michael

PB - Springer

CY - Berlin

T2 - 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007

Y2 - 24 March 2007 through 1 April 2007

ER -

Katoen JP, Kemna T, Zapreev I, 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: 13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. Berlin: Springer. 2007. p. 87-101. (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues). doi: 10.1007/978-3-540-71209-1_9

Bisimulation minimisation mostly speeds up probabilistic model checking

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this