Faster and symbolic CTMC model checking

Joost P. Katoen, Marta Kwiatkowska, Gethin Norman, David Parker

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

    46 Citations (Scopus)

    Abstract

    This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.
    Original languageEnglish
    Title of host publicationProcess Algebra and Probabilistic Methods, Performance Modeling and Verification
    Subtitle of host publicationJoint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings
    EditorsS. Gilmore, L. de Alfaro
    Place of PublicationBerlin
    PublisherSpringer
    Pages23-38
    Number of pages16
    ISBN (Print)3-540-42556-X
    DOIs
    Publication statusPublished - 2001
    EventProcess Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001 - Aachen, Germany
    Duration: 12 Sep 200114 Sep 2001

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume2165
    ISSN (Print)0302-9743

    Conference

    ConferenceProcess Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001
    CountryGermany
    CityAachen
    Period12/09/0114/09/01

    Keywords

    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • FMT-BDD: BINARY DECISION DIAGRAMS
    • FMT-PM: PROBABILISTIC METHODS
    • FMT-MC: MODEL CHECKING
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-TOOLS
    • EWI-6449
    • IR-63281
    • METIS-203851

    Fingerprint Dive into the research topics of 'Faster and symbolic CTMC model checking'. Together they form a unique fingerprint.

  • Cite this

    Katoen, J. P., Kwiatkowska, M., Norman, G., & Parker, D. (2001). Faster and symbolic CTMC model checking. In S. Gilmore, & L. de Alfaro (Eds.), Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings (pp. 23-38). (Lecture Notes in Computer Science; Vol. 2165). Berlin: Springer. https://doi.org/10.1007/3-540-44804-7_2