Model Checking Continuous-Time Markov Chains by Transient Analysis

Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen

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

    113 Citations (Scopus)
    190 Downloads (Pure)

    Abstract

    The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branching time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form Pp(Φ1 UI Φ2), for state formulas Φ1 and Φ2, comparison operator , probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.
    Original languageEnglish
    Title of host publicationComputer Aided Verification
    Subtitle of host publication12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings
    EditorsE. Allen Emerson, Aravinda Prasad Sistla
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages358-372
    Number of pages15
    ISBN (Electronic)978-3-540-45047-4
    ISBN (Print)978-3-540-67770-3
    DOIs
    Publication statusPublished - 2000
    Event12th International Conference on Computer Aided Verification, CAV 2000 - Chicago, United States
    Duration: 15 Jul 200019 Jul 2000
    Conference number: 12

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume1855
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference12th International Conference on Computer Aided Verification, CAV 2000
    Abbreviated titleCAV
    Country/TerritoryUnited States
    CityChicago
    Period15/07/0019/07/00

    Keywords

    • FMT-MC: MODEL CHECKING
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-PM: PROBABILISTIC METHODS

    Fingerprint

    Dive into the research topics of 'Model Checking Continuous-Time Markov Chains by Transient Analysis'. Together they form a unique fingerprint.

    Cite this