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

    47 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 languageUndefined
    Title of host publicationProcess Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001
    EditorsS. Gilmore, L. de Alfaro
    Place of PublicationBerlin
    PublisherSpringer
    Pages23-38
    Number of pages16
    ISBN (Print)3-540-42556-X
    DOIs
    Publication statusPublished - 2001

    Publication series

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

    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

    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 (pp. 23-38). (Lecture Notes in Computer Science; Vol. 2165). Berlin: Springer. https://doi.org/10.1007/3-540-44804-7_2
    Katoen, Joost P. ; Kwiatkowska, Marta ; Norman, Gethin ; Parker, David. / Faster and symbolic CTMC model checking. Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. editor / S. Gilmore ; L. de Alfaro. Berlin : Springer, 2001. pp. 23-38 (Lecture Notes in Computer Science).
    @inproceedings{f9ce3196db8a4f98b88c847c25d44bd1,
    title = "Faster and symbolic CTMC model checking",
    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.",
    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",
    author = "Katoen, {Joost P.} and Marta Kwiatkowska and Gethin Norman and David Parker",
    year = "2001",
    doi = "10.1007/3-540-44804-7_2",
    language = "Undefined",
    isbn = "3-540-42556-X",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "23--38",
    editor = "S. Gilmore and {de Alfaro}, L.",
    booktitle = "Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001",

    }

    Katoen, JP, 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. Lecture Notes in Computer Science, vol. 2165, Springer, Berlin, pp. 23-38. https://doi.org/10.1007/3-540-44804-7_2

    Faster and symbolic CTMC model checking. / Katoen, Joost P.; Kwiatkowska, Marta; Norman, Gethin; Parker, David.

    Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. ed. / S. Gilmore; L. de Alfaro. Berlin : Springer, 2001. p. 23-38 (Lecture Notes in Computer Science; Vol. 2165).

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

    TY - GEN

    T1 - Faster and symbolic CTMC model checking

    AU - Katoen, Joost P.

    AU - Kwiatkowska, Marta

    AU - Norman, Gethin

    AU - Parker, David

    PY - 2001

    Y1 - 2001

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

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

    KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

    KW - FMT-BDD: BINARY DECISION DIAGRAMS

    KW - FMT-PM: PROBABILISTIC METHODS

    KW - FMT-MC: MODEL CHECKING

    KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    KW - FMT-TOOLS

    KW - EWI-6449

    KW - IR-63281

    KW - METIS-203851

    U2 - 10.1007/3-540-44804-7_2

    DO - 10.1007/3-540-44804-7_2

    M3 - Conference contribution

    SN - 3-540-42556-X

    T3 - Lecture Notes in Computer Science

    SP - 23

    EP - 38

    BT - Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001

    A2 - Gilmore, S.

    A2 - de Alfaro, L.

    PB - Springer

    CY - Berlin

    ER -

    Katoen JP, Kwiatkowska M, Norman G, Parker D. Faster and symbolic CTMC model checking. In Gilmore S, de Alfaro L, editors, Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. Berlin: Springer. 2001. p. 23-38. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-44804-7_2