Abstract
Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.
Original language | English |
---|---|
Title of host publication | Process Algebra and Probabilistic Methods. Performance Modelling and Verification |
Subtitle of host publication | Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001, Proceedings |
Editors | Luca de Alfaro, Stephen Gilmore |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 57-70 |
Number of pages | 14 |
ISBN (Electronic) | 978-3-540-44804-4 |
ISBN (Print) | 978-3-540-42556-4 |
DOIs | |
Publication status | Published - 2001 |
Event | Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001 - Aachen, Germany Duration: 12 Sep 2001 → 14 Sep 2001 |
Workshop
Workshop | Joint International Workshop on Process Algebra and Probabilistic Methods & Probabilistic Methods in Verification, PAPM-PROBMIV 2001 |
---|---|
Abbreviated title | PAPM-PROBMIV |
Country/Territory | Germany |
City | Aachen |
Period | 12/09/01 → 14/09/01 |
Keywords
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-MC: MODEL CHECKING
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
- FMT-PM: PROBABILISTIC METHODS