Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

T. Chen, Tingting Han, Joost P. Katoen, Alexandru Mereacre

Research output: Contribution to journalArticleAcademicpeer-review

38 Citations (Scopus)
26 Downloads (Pure)

Abstract

We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.
Original languageUndefined
Pages (from-to)12:1-12:34
Number of pages34
JournalLogical methods in computer science
Volume7
Issue number1-12
DOIs
Publication statusPublished - 2011

Keywords

  • IR-79353
  • EWI-21245

Cite this

Chen, T. ; Han, Tingting ; Katoen, Joost P. ; Mereacre, Alexandru. / Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. In: Logical methods in computer science. 2011 ; Vol. 7, No. 1-12. pp. 12:1-12:34.
@article{0eac23086a054fb5a4ef7452a71bf4ac,
title = "Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications",
abstract = "We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.",
keywords = "IR-79353, EWI-21245",
author = "T. Chen and Tingting Han and Katoen, {Joost P.} and Alexandru Mereacre",
note = "Open Access",
year = "2011",
doi = "10.2168/LMCS-7(1:12)2011",
language = "Undefined",
volume = "7",
pages = "12:1--12:34",
journal = "Logical methods in computer science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "1-12",

}

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. / Chen, T.; Han, Tingting; Katoen, Joost P.; Mereacre, Alexandru.

In: Logical methods in computer science, Vol. 7, No. 1-12, 2011, p. 12:1-12:34.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

AU - Chen, T.

AU - Han, Tingting

AU - Katoen, Joost P.

AU - Mereacre, Alexandru

N1 - Open Access

PY - 2011

Y1 - 2011

N2 - We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.

AB - We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or Muller acceptance conditions. The central question that we address is: what is the probability of the set of paths of C that are accepted by A, i.e., the likelihood that C satisfies A? It is shown that under finite acceptance criteria this equals the reachability probability in a finite piecewise deterministic Markov process (PDP), whereas for Muller acceptance criteria it coincides with the reachability probability of terminal strongly connected components in such a PDP. Qualitative verification is shown to amount to a graph analysis of the PDP. Reachability probabilities in our PDPs are then characterized as the least solution of a system of Volterra integral equations of the second type and are shown to be approximated by the solution of a system of partial differential equations. For single-clock DTA, this integral equation system can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations. As the coefficients are in fact transient probabilities in CTMCs, this result implies that standard algorithms for CTMC analysis suffice to verify single-clock DTA specifications.

KW - IR-79353

KW - EWI-21245

U2 - 10.2168/LMCS-7(1:12)2011

DO - 10.2168/LMCS-7(1:12)2011

M3 - Article

VL - 7

SP - 12:1-12:34

JO - Logical methods in computer science

JF - Logical methods in computer science

SN - 1860-5974

IS - 1-12

ER -