Symbolic Model Checking for Probabilistic Processes

Christel BaierChristel Baier, Edmund M. ClarkeEdmund M. Clarke, Vasiliki Hartonas-GarmhausenVasiliki Hartonas-Garmhausen, Marta Z. KwiatkowskaMarta Z. Kwiatkowska, Mark RyanMark Ryan

DOI Link

Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, Mark Ryan
Symbolic Model Checking for Probabilistic Processes
24th International Colloquium on Automata, Languages and Programming (ICALP), volume 1256 of Lecture Notes in Computer Science, 430--440, 1997. Springer

Details
Bibtex

KurzfassungAbstract
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 systems 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 linear 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].
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-63165-8_199.

@inproceedings{BCHKR1997,
  author    = {Christel Baier and Edmund M. Clarke and Vasiliki
               Hartonas-Garmhausen and Marta Z. Kwiatkowska and Mark Ryan},
  title     = {Symbolic Model Checking for Probabilistic Processes},
  booktitle = {24th International Colloquium on Automata, Languages and
               Programming (ICALP)},
  series    = {Lecture Notes in Computer Science},
  volume    = {1256},
  publisher = {Springer},
  year      = {1997},
  pages     = {430--440},
  doi       = {10.1007/3-540-63165-8_199}
}