Symbolic Model Checking for Probabilistic Processes
From International Center for Computational Logic
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
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
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
- 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
@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}
}