Model Checking Continuous-Time Markov Chains by Transient Analysis

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

Research output: Contribution to conferencePaperAcademicpeer-review

96 Citations (Scopus)
37 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

Fingerprint

Model checking
Transient analysis
Markov processes
Specifications
Temporal logic
Mathematical operators

Keywords

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

Cite this

Baier, C., Haverkort, B., Hermanns, H., & Katoen, J. P. (2000). Model Checking Continuous-Time Markov Chains by Transient Analysis. 358-372. Paper presented at 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, United States. https://doi.org/10.1007/10722167_28
Baier, Christel ; Haverkort, Boudewijn ; Hermanns, Holger ; Katoen, Joost Pieter. / Model Checking Continuous-Time Markov Chains by Transient Analysis. Paper presented at 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, United States.15 p.
@conference{efb2c1bdb5c743b08d5ec893efb6ba9d,
title = "Model Checking Continuous-Time Markov Chains by Transient Analysis",
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.",
keywords = "EWI-6442, FMT-MC: MODEL CHECKING, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-PM: PROBABILISTIC METHODS, IR-63277",
author = "Christel Baier and Boudewijn Haverkort and Holger Hermanns and Katoen, {Joost Pieter}",
year = "2000",
doi = "10.1007/10722167_28",
language = "English",
pages = "358--372",
note = "12th International Conference on Computer Aided Verification, CAV 2000, CAV ; Conference date: 15-07-2000 Through 19-07-2000",

}

Baier, C, Haverkort, B, Hermanns, H & Katoen, JP 2000, 'Model Checking Continuous-Time Markov Chains by Transient Analysis' Paper presented at 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, United States, 15/07/00 - 19/07/00, pp. 358-372. https://doi.org/10.1007/10722167_28

Model Checking Continuous-Time Markov Chains by Transient Analysis. / Baier, Christel; Haverkort, Boudewijn; Hermanns, Holger; Katoen, Joost Pieter.

2000. 358-372 Paper presented at 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, United States.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Model Checking Continuous-Time Markov Chains by Transient Analysis

AU - Baier, Christel

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost Pieter

PY - 2000

Y1 - 2000

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

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

KW - EWI-6442

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-PM: PROBABILISTIC METHODS

KW - IR-63277

U2 - 10.1007/10722167_28

DO - 10.1007/10722167_28

M3 - Paper

SP - 358

EP - 372

ER -

Baier C, Haverkort B, Hermanns H, Katoen JP. Model Checking Continuous-Time Markov Chains by Transient Analysis. 2000. Paper presented at 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, United States. https://doi.org/10.1007/10722167_28