Conference item

### Time−Bounded Verification of CTMCs Against Real−Time Specifications

Abstract:

Abstract. In this paper we study time-bounded verification of a finite continuous-timeMarkov chain (CTMC) C against a real-time specification, provided either as a metric temporal logic (MTL) property 'φ', or as a timed automaton (TA) A. The key question is: what is the probability of the set of timed paths of C that satisfy 'φ' (or are accepted by A) over a time interval of fixed, bounded length? We provide approximation algorithms to solve these problems. We first derive a bound N such that...

### Authors

Publisher:
Springer
Publication date:
2011-01-01
URN:
Local pid:
cs:5085