Conference item icon

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

Expand abstract

Actions


Authors


Publisher:
Springer
Publication date:
2011-01-01
URN:
uuid:32e8db2d-5775-4dee-9fae-cfef2eadf8a0
Local pid:
cs:5085

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP