Name
Abstract | ||
|---|---|---|
We introduce a symbolic model checking procedure for Probabilistic Computation Tree Logic PCTL over labelled Markov chains as models. Model checking for probabilistic logics typically involves solving linear equation sys- tems in order to ascertain the probability of a given formula holding in a state. Our algorithm is based on the idea of representing the matrices used in the lin- ear equation systems by Multi-Terminal Binary Decision Diagrams (MTBDDs) introduced in Clarke et al (14). Our procedure, based on the algorithm used by Hansson and Jonsson (24), uses BDDs to represent formulas and MTBDDs to represent Markov chains, and is efficient because it avoids explicit state space construction. A PCTL model checker is being implemented in Verus (9). |
Year | DOI | Venue |
|---|---|---|
1997 | 10.1007/3-540-63165-8_199 | ICALP |
Keywords | Field | DocType |
probabilistic processes,symbolic model checking | Discrete mathematics,Combinatorics,Model checking,Algorithmics,Computer science,Markov chain,Binary decision diagram,Probabilistic CTL,Algorithm,Probabilistic logic,State space,Probabilistic automaton | Conference |
Volume | ISSN | ISBN |
1256 | 0302-9743 | 3-540-63165-8 |
Citations | PageRank | References |
87 | 5.84 | 27 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christel Baier | 1 | 3053 | 185.85 |
| Edmund M. Clarke | 2 | 20645 | 2418.32 |
| Vassili Hartonas-Garmhausen | 3 | 1250 | 112.12 |
| Marta Z. Kwiatkowska | 4 | 6118 | 322.21 |
| Mark Ryan | 5 | 152 | 18.68 |