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

    79 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
    Event13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007 - Braga, Portugal
    Duration: 24 Mar 20071 Apr 2007
    Conference number: 13

    Publication series

    NameLecture notes in computer science
    PublisherSpringer
    Number2
    Volume4424

    Conference

    Conference13th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS 2007
    Abbreviated titleTACAS
    CountryPortugal
    CityBraga
    Period24/03/071/04/07

    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