Abstract
The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branching time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form Pp(Φ1 UI Φ2), for state formulas Φ1 and Φ2, comparison operator , probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.
Original language | English |
---|---|
Title of host publication | Computer Aided Verification |
Subtitle of host publication | 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings |
Editors | E. Allen Emerson, Aravinda Prasad Sistla |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 358-372 |
Number of pages | 15 |
ISBN (Electronic) | 978-3-540-45047-4 |
ISBN (Print) | 978-3-540-67770-3 |
DOIs | |
Publication status | Published - 2000 |
Event | 12th International Conference on Computer Aided Verification, CAV 2000 - Chicago, United States Duration: 15 Jul 2000 → 19 Jul 2000 Conference number: 12 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 1855 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 12th International Conference on Computer Aided Verification, CAV 2000 |
---|---|
Abbreviated title | CAV |
Country/Territory | United States |
City | Chicago |
Period | 15/07/00 → 19/07/00 |
Keywords
- FMT-MC: MODEL CHECKING
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-PM: PROBABILISTIC METHODS