Quantitative model checking of continuous-time Markov chains against timed automata specifications

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

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

29 Citations (Scopus)
30 Downloads (Pure)

Abstract

We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.
Original languageUndefined
Title of host publication2009 24th Annual IEEE Symposium on Logic In Computer Science
Place of PublicationPiscataway
PublisherIEEE Computer Society
Pages309-318
Number of pages10
ISBN (Print)978-0-7695-3746-7
DOIs
Publication statusPublished - Aug 2009
Event24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009 - UCLA, Los Angeles, United States
Duration: 11 Aug 200914 Aug 2009
Conference number: 24

Publication series

Name
PublisherIEEE Computer Society Press
ISSN (Print)1043-6871

Conference

Conference24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009
Abbreviated titleLICS
CountryUnited States
CityLos Angeles
Period11/08/0914/08/09

Keywords

  • METIS-264047
  • IR-68256
  • EWI-16106
  • FMT-PM: PROBABILISTIC METHODS
  • FMT-MC: MODEL CHECKING

Cite this

Chen, T., Han, T., Katoen, J. P., & Mereacre, A. (2009). Quantitative model checking of continuous-time Markov chains against timed automata specifications. In 2009 24th Annual IEEE Symposium on Logic In Computer Science (pp. 309-318). [10.1109/LICS.2009.21] Piscataway: IEEE Computer Society. https://doi.org/10.1109/LICS.2009.21
Chen, T. ; Han, Tingting ; Katoen, Joost P. ; Mereacre, Alexandru. / Quantitative model checking of continuous-time Markov chains against timed automata specifications. 2009 24th Annual IEEE Symposium on Logic In Computer Science. Piscataway : IEEE Computer Society, 2009. pp. 309-318
@inproceedings{e61ff58240ed425e96b12f31230493e9,
title = "Quantitative model checking of continuous-time Markov chains against timed automata specifications",
abstract = "We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.",
keywords = "METIS-264047, IR-68256, EWI-16106, FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING",
author = "T. Chen and Tingting Han and Katoen, {Joost P.} and Alexandru Mereacre",
note = "10.1109/LICS.2009.21",
year = "2009",
month = "8",
doi = "10.1109/LICS.2009.21",
language = "Undefined",
isbn = "978-0-7695-3746-7",
publisher = "IEEE Computer Society",
pages = "309--318",
booktitle = "2009 24th Annual IEEE Symposium on Logic In Computer Science",
address = "United States",

}

Chen, T, Han, T, Katoen, JP & Mereacre, A 2009, Quantitative model checking of continuous-time Markov chains against timed automata specifications. in 2009 24th Annual IEEE Symposium on Logic In Computer Science., 10.1109/LICS.2009.21, IEEE Computer Society, Piscataway, pp. 309-318, 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009, Los Angeles, United States, 11/08/09. https://doi.org/10.1109/LICS.2009.21

Quantitative model checking of continuous-time Markov chains against timed automata specifications. / Chen, T.; Han, Tingting; Katoen, Joost P.; Mereacre, Alexandru.

2009 24th Annual IEEE Symposium on Logic In Computer Science. Piscataway : IEEE Computer Society, 2009. p. 309-318 10.1109/LICS.2009.21.

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

TY - GEN

T1 - Quantitative 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 - 10.1109/LICS.2009.21

PY - 2009/8

Y1 - 2009/8

N2 - We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.

AB - We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.

KW - METIS-264047

KW - IR-68256

KW - EWI-16106

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

U2 - 10.1109/LICS.2009.21

DO - 10.1109/LICS.2009.21

M3 - Conference contribution

SN - 978-0-7695-3746-7

SP - 309

EP - 318

BT - 2009 24th Annual IEEE Symposium on Logic In Computer Science

PB - IEEE Computer Society

CY - Piscataway

ER -

Chen T, Han T, Katoen JP, Mereacre A. Quantitative model checking of continuous-time Markov chains against timed automata specifications. In 2009 24th Annual IEEE Symposium on Logic In Computer Science. Piscataway: IEEE Computer Society. 2009. p. 309-318. 10.1109/LICS.2009.21 https://doi.org/10.1109/LICS.2009.21