Model-checking algorithms for continuous-time Markov chains

Christel Baier, Boudewijn R.H.M. Haverkort, H. Hermanns, Joost P. Katoen

Research output: Contribution to journalArticleScientificpeer-review

Abstract

Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an 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 then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.
Original languageEnglish
Pages (from-to)524-541
Number of pages18
JournalIEEE Transactions on Software Engineering
Volume29
Issue number6
DOIs
Publication statusPublished - Jun 2003
Externally publishedYes

Fingerprint

Model checking
Markov processes
Mathematical operators
Temporal logic
Linear equations
Transient analysis
Integral equations

Keywords

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

Cite this

Baier, Christel ; Haverkort, Boudewijn R.H.M. ; Hermanns, H. ; Katoen, Joost P. / Model-checking algorithms for continuous-time Markov chains. In: IEEE Transactions on Software Engineering. 2003 ; Vol. 29, No. 6. pp. 524-541.
@article{7df7ec700a2543eaad9a006f2e8220df,
title = "Model-checking algorithms for continuous-time Markov chains",
abstract = "Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an 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 then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.",
keywords = "IR-63267, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, EWI-6402, FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING",
author = "Christel Baier and Haverkort, {Boudewijn R.H.M.} and H. Hermanns and Katoen, {Joost P.}",
note = "M1 - 10.1109/TSE.2003.1205180",
year = "2003",
month = "6",
doi = "10.1109/TSE.2003.1205180",
language = "English",
volume = "29",
pages = "524--541",
journal = "IEEE Transactions on Software Engineering",
issn = "0098-5589",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
number = "6",

}

Model-checking algorithms for continuous-time Markov chains. / Baier, Christel; Haverkort, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P.

In: IEEE Transactions on Software Engineering, Vol. 29, No. 6, 06.2003, p. 524-541.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

T1 - Model-checking algorithms for continuous-time Markov chains

AU - Baier, Christel

AU - Haverkort, Boudewijn R.H.M.

AU - Hermanns, H.

AU - Katoen, Joost P.

N1 - M1 - 10.1109/TSE.2003.1205180

PY - 2003/6

Y1 - 2003/6

N2 - Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an 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 then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.

AB - Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an 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 then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.

KW - IR-63267

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - EWI-6402

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

U2 - 10.1109/TSE.2003.1205180

DO - 10.1109/TSE.2003.1205180

M3 - Article

VL - 29

SP - 524

EP - 541

JO - IEEE Transactions on Software Engineering

JF - IEEE Transactions on Software Engineering

SN - 0098-5589

IS - 6

ER -