Abstract
Markov chains are widely used in the context of
performance and reliability evaluation of systems of various
nature. Model checking of such chains with respect to
a given (branching) temporal logic formula has been proposed
for both the discrete [8] and the continuous time setting
[1], [3]. In this short paper, we describe the prototype
model checker $E \vdash M C^2$ for discrete and continuous-time
Markov chains, where properties are expressed in appropriate
extensions of CTL.We illustrate the general benefits
of this approach and discuss the structure of the tool.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001 |
| Place of Publication | Veldhoven, the Netherlands |
| Publisher | STW |
| Pages | 83-88 |
| Number of pages | 6 |
| ISBN (Print) | 90-73461-27-X |
| Publication status | Published - 2001 |
| Event | 2nd PROGRESS Workshop on Embedded Systems 2001 - Veldhoven, Netherlands Duration: 18 Oct 2001 → 18 Oct 2001 Conference number: 2 |
Workshop
| Workshop | 2nd PROGRESS Workshop on Embedded Systems 2001 |
|---|---|
| Abbreviated title | PROGRESS |
| Country/Territory | Netherlands |
| City | Veldhoven |
| Period | 18/10/01 → 18/10/01 |
Keywords
- FMT-PM: PROBABILISTIC METHODS
- FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
- FMT-MC: MODEL CHECKING
- FMT-TOOLS
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS