### Abstract

Original language | Undefined |
---|---|

Title of host publication | 2009 24th Annual IEEE Symposium on Logic In Computer Science |

Place of Publication | Piscataway |

Publisher | IEEE Computer Society |

Pages | 309-318 |

Number of pages | 10 |

ISBN (Print) | 978-0-7695-3746-7 |

DOIs | |

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

### Cite this

*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

}

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

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