Time−Bounded Verification of CTMCs Against Real−Time Specifications
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...
| Main Authors: | , , , |
|---|---|
| Formato: | Conference item |
| Publicado em: |
Springer
2011
|
| _version_ | 1826266296682020864 |
|---|---|
| author | Chen, T Diciolla, M Kwiatkowska, M Mereacre, A |
| author_facet | Chen, T Diciolla, M Kwiatkowska, M Mereacre, A |
| author_sort | Chen, T |
| collection | OXFORD |
| description | 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 timed paths of C with at most N discrete jumps are sufficient to approximate the desired probability up to 'ε'. Then, for each discrete (untimed) path 'ς' of length at most N, we generate timed constraints over variables determining the residence time of each state along 'ς', depending on the real-time specification under consideration. The probability of the set of timed paths, determined by the discrete path and the associated timed constraints, can thus be formulated as a multidimensional integral. Summing up all such probabilities yields the result. For MTL, we consider both the continuous and the pointwise semantics. The approximation algorithms differ mainly in constraints generation for the two types of specifications. |
| first_indexed | 2024-03-06T20:36:45Z |
| format | Conference item |
| id | oxford-uuid:32e8db2d-5775-4dee-9fae-cfef2eadf8a0 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:36:45Z |
| publishDate | 2011 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:32e8db2d-5775-4dee-9fae-cfef2eadf8a02022-03-26T13:16:54ZTime−Bounded Verification of CTMCs Against Real−Time SpecificationsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:32e8db2d-5775-4dee-9fae-cfef2eadf8a0Department of Computer ScienceSpringer2011Chen, TDiciolla, MKwiatkowska, MMereacre, AAbstract. 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 timed paths of C with at most N discrete jumps are sufficient to approximate the desired probability up to 'ε'. Then, for each discrete (untimed) path 'ς' of length at most N, we generate timed constraints over variables determining the residence time of each state along 'ς', depending on the real-time specification under consideration. The probability of the set of timed paths, determined by the discrete path and the associated timed constraints, can thus be formulated as a multidimensional integral. Summing up all such probabilities yields the result. For MTL, we consider both the continuous and the pointwise semantics. The approximation algorithms differ mainly in constraints generation for the two types of specifications. |
| spellingShingle | Chen, T Diciolla, M Kwiatkowska, M Mereacre, A Time−Bounded Verification of CTMCs Against Real−Time Specifications |
| title | Time−Bounded Verification of CTMCs Against Real−Time Specifications |
| title_full | Time−Bounded Verification of CTMCs Against Real−Time Specifications |
| title_fullStr | Time−Bounded Verification of CTMCs Against Real−Time Specifications |
| title_full_unstemmed | Time−Bounded Verification of CTMCs Against Real−Time Specifications |
| title_short | Time−Bounded Verification of CTMCs Against Real−Time Specifications |
| title_sort | time bounded verification of ctmcs against real time specifications |
| work_keys_str_mv | AT chent timeboundedverificationofctmcsagainstrealtimespecifications AT diciollam timeboundedverificationofctmcsagainstrealtimespecifications AT kwiatkowskam timeboundedverificationofctmcsagainstrealtimespecifications AT mereacrea timeboundedverificationofctmcsagainstrealtimespecifications |