Abstract
This paper reports on experimental results with symbolic model checking of probabilistic processes based on Multi-Terminal Binary Decision Diagrams (MTBDDs). We consider concurrent probabilistic systems as models; these allow nondeterministic choice between probability distributions and are particularly well suited to modelling distributed systems with probabilistic behaviour, e.g. randomized consensus algorithms and probabilistic failures. As a specification formalism we use the probabilistic branching-time temporal logic PBTL which allows one to express properties such as “under any scheduling of nondeterministic choices, the probability of φ holding until ψ is true is at least 0.78/at most 0.04”. We adapt the Kronecker representation of (Plateau 1985), which yields a very compact MTBDD encoding of the system. We implement an experimental model checker using the CUDD package and demonstrate that model construction and reachability-based model checking is possible in a matter of seconds for certain classes of systems consisting of up to 1030 states.
Supported in part by EPSRC grant GR/M04617.
Supported in part by EPSRC grant GR/M13046.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
I. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and their Applications. Journal of Formal Methods in Systems Design, 10(2/3):171–206, 1997. 396, 397, 401, 405
C. Baier. On algorithmic verification methods for probabilistic systems. Habilitation thesis, 1998. 396, 397, 399, 400, 401
C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Proceedings, 24th ICALP, volume 1256 of LNCS, pages 430–440. Springer-Verlag, 1997. 396, 397, 401
C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR’99, volume 1664 of LNCS, pages 146–161. Springer-Verlag, 1999. 396, 407
C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125–155, 1998. 396, 397, 398, 399, 400
J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of uppaal. In Proceedings of the International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July 1998. 396
D. Bertsekas. Dynamic Programming and Optimal Control. Athena Scientific, 1995. 396
A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proceedings, FST&TCS, volume 1026 of LNCS, pages 499–513. Springer-Verlag, 1995. 396, 398, 399
M. Bozga and O. Maler. On the representation of probabilities over structured domains. In Proc. CAV’99, 1999. Available as Volume 1633 of LNCS. 396, 407
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In LICS’90, June 1990. 395
G. Ciardo and A. Miner. SMART: Simulation and markovian analyzer for reliability and timing. In Tools Descriptions from PNPM’97, pages 41–43, 1997. 397
G. Ciardo and A. Miner. A data structure for the efficient Kronecker solution of GSPNs. In Proc. PNPM’99, 1999. 406, 407
E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Proceedings, 10th Annual Symp. on Principles of Programming Languages, 1983. 398, 399
E. Clarke, M. Fujita, P. McGeer, J. Yang, and X. Zhao. Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation. In International Workshop on Logic Synthesis, 1993. 396, 401, 405
C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events. In Proc. ICALP’90, volume 443 of LNCS, pages 336–349. Springer-Verlag, 1990. 396, 400
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857–907, 1995. 398, 400
L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In Proc. LICS’98, pages 454–465, 1998. 396
L. de Alfaro. Stochastic transition systems. In Proc. CONCUR’98, volume 1466 of LNCS. Springer-Verlag, 1998. 396
L. de Alfaro. Computing minimum and maximum reachability times in probabilistic systems. In Proc. CONCUR’99, volume 1664 of LNCS, 1999. 397, 400
L. de Alfaro. From fairness to chance. In Proc. PROBMIV’98, volume 21 of ENTCS. Elsevier, 1999. 398
G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on CAD, 15(12):1479–1493, 1996. 397
H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6:512–535, 1994. 396, 398
H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi Terminal Binary Decision Diagrams to represent and analyse continuous time Markov chains. In Proc. NSMC’99, 1999. 397, 405
M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic systems using MTBDDs and simplex. Technical Report CSR-99-1, University of Birmingham, 1999. 397
K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 395
B. Plateau. On the Stochastic Structure of Parallelism and Synchronisation Models for Distributed Algorithms. In Proc. 1985 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems, pages 147–153, May 1985. 397, 402, 403
B. Plateau, J. M. Fourneau, and K. H. Lee. PEPS: a package for solving complex Markov models of parallel systems. In R. Puigjaner and D. Potier, editors, Modelling techniques and tools for computer performance evaluation, 1988. 397
A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1:53–72, 1986. 396, 406
R. Segala. Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. 398
M. Siegle. Compact representation of large performability models based on extended BDDs. In Fourth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS4), pages 77–80, 1998. 405
F. Somenzi. CUDD: CU decision diagram package. Public software, Colorado University, Boulder, 1997. 396, 397, 405
M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings, FOCS’85, pages 327–338. IEEE Press, 1987. 396, 398
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R. (2000). Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_27
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive