tr-announce August 2009

tr-announce@lists.rwth-aachen.de

1 participants
1 discussions

2009-02: Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

by Carsten Fuhs

The following technical report is available from http://aib.informatik.rwth-aachen.de: Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre AIB 2009-02 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.

15 years

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce August 2009