Model Checking Continuous-Time Markov Chains by Transient Analysis

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

    Research output: Contribution to conferencePaperAcademicpeer-review

    99 Citations (Scopus)
    67 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
    Pages358-372
    Number of pages15
    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

    Conference

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

    Keywords

    • EWI-6442
    • FMT-MC: MODEL CHECKING
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-PM: PROBABILISTIC METHODS
    • IR-63277

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

    Cite this