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

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

doi:10.1109/LICS.2009.21

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 proceeding › Conference contribution › Academic › peer-review

34 Citations (Scopus)

186 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 language	Undefined
Title of host publication	2009 24th Annual IEEE Symposium on Logic In Computer Science
Place of Publication	Piscataway
Publisher	IEEE
Pages	309-318
Number of pages	10
ISBN (Print)	978-0-7695-3746-7
DOIs	https://doi.org/10.1109/LICS.2009.21
Publication status	Published - Aug 2009
Event	24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009 - UCLA, Los Angeles, United States Duration: 11 Aug 2009 → 14 Aug 2009 Conference number: 24

Publication series

Name
Publisher	IEEE Computer Society Press
ISSN (Print)	1043-6871

Conference

Conference	24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009
Abbreviated title	LICS
Country/Territory	United States
City	Los Angeles
Period	11/08/09 → 14/08/09

Keywords

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

Access to Document

10.1109/LICS.2009.21

Cite this

@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 ; 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009 ; Conference date: 11-08-2009 Through 14-08-2009",

year = "2009",

month = aug,

doi = "10.1109/LICS.2009.21",

language = "Undefined",

isbn = "978-0-7695-3746-7",

publisher = "IEEE",

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, Piscataway, pp. 309-318, 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009, Los Angeles, California, 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. et al.
2009 24th Annual IEEE Symposium on Logic In Computer Science. Piscataway: IEEE, 2009. p. 309-318 10.1109/LICS.2009.21.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 - Conference code: 24

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

CY - Piscataway

T2 - 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009

Y2 - 11 August 2009 through 14 August 2009

ER -