Abstract
Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.
Original language | Undefined |
---|---|
Title of host publication | 16th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 |
Editors | J. Esparza, R. Majumdar |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 53-68 |
Number of pages | 16 |
ISBN (Print) | 978-3-642-12001-5 |
DOIs | |
Publication status | Published - 1 Apr 2010 |
Event | 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 - Paphos, Cyprus Duration: 20 Mar 2010 → 28 Mar 2010 Conference number: 16 http://www.etaps.org/2010/Conf/conf-frame-tacas.html |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Volume | 6015 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010 |
---|---|
Abbreviated title | TACAS |
Country/Territory | Cyprus |
City | Paphos |
Period | 20/03/10 → 28/03/10 |
Internet address |
Keywords
- METIS-270938
- EWI-18211
- IR-72599