Approximative Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract)

Christel Baier, Joost-Pieter Katoen, Holger Hermanns

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

    162 Citations (Scopus)

    Abstract

    This paper presents a symbolic model checking algorithm for continuous-time Markov chains for an extension of the continuous stochastic logic CSL of Aziz et al. [1] The considered logic contains a time-bounded until-operator and a novel operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady state-operator) and a Volterra integral equation system for time-bounded until. We propose a symbolic approximate method for solving the integrals using MTDDs (multi-terminal decision diagrams), a generalisation of MTBDDs. These new structures are suitable for numerical integration using quadrature formulas based on equally-spaced abscissas, like trapezoidal, Simpson and Romberg integration schemes.
    Original languageEnglish
    Title of host publicationCONCUR’99 Concurrency Theory
    Subtitle of host publication10th International Conference Eindhoven, The Netherlands, August 24—27, 1999 Proceedings
    EditorsJos C.M. Baeten, Sjouke Mauw
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages146-162
    Number of pages16
    ISBN (Electronic)978-3-540-48320-5
    ISBN (Print)978-3-540-66425-3
    DOIs
    Publication statusPublished - 1999
    Event10th International Conference on Concurrency Theory, CONCUR 1999 - Eindhoven, Netherlands
    Duration: 24 Aug 199927 Aug 1999
    Conference number: 10

    Publication series

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

    Conference

    Conference10th International Conference on Concurrency Theory, CONCUR 1999
    Abbreviated titleCONCUR
    Country/TerritoryNetherlands
    CityEindhoven
    Period24/08/9927/08/99

    Keywords

    • FMT-MC: MODEL CHECKING
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • FMT-BDD: BINARY DECISION DIAGRAMS

    Fingerprint

    Dive into the research topics of 'Approximative Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract)'. Together they form a unique fingerprint.

    Cite this