On the Representation of Probabilities over Structured Domains

  • Marius Bozga
  • Oded Maler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1633)


In this paper we extend one of the main tools used in verification of discrete systems, namely Binary Decision Diagrams (BDD), to treat probabilistic transition systems. We show how probabilistic vectors and matrices can be represented canonically and succinctly using probabilistic trees and graphs, and how simulation of large-scale probabilistic systems can be performed. We consider this work as an important contribution of the verification community to numerous domains which need to manipulate very large matrices.


  1. [B86]
    R.E. Bryant, Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. on Computers C-35, 677–691, 1986.CrossRefGoogle Scholar
  2. [BCM+93]_ J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, Symbolic Model-Checking: 1020 States and Beyond, Information and Computation 98, 142–70, 1992.MathSciNetCrossRefGoogle Scholar
  3. [BDH99]
    C. Boutilier, T. Dean and S. Hanks, Decision Theoretic Planning: Structural Assumptions and Computational Leverage, J. of AI Research (to appear).Google Scholar
  4. [BFG+93]_ R.I. Bahar, E.A. Frohm, C.M. Ganoa, G.D. Hachtel, E. Macii, A. Pardo and F. Somenzi, Algebraic Decision Diagrams and their Applications, Proc. ICCAD’93, 188–191, 1993.Google Scholar
  5. [BCG+97]_ C. Baier, E. Clarke, V. Garmhausen-Hartonas, M. Kwiatkowska and M. Ryan, Symbolic Model Checking for Probabilistic Processes, in P. Degano, R. Gorrieri and A. Marchetti-Spaccamela (Eds.), Proc. ICALP’97, 430–440, LNCS 1256, Springer, 1997.Google Scholar
  6. [CFM+93]_ E. M. Clarke, M. Fujita, P. C. McGeer, K. L. Mcmillan and J. C.-Y. Yang, Multi-terminal Binary decision Diagrams: An Efficient Data-structure for Matrix Representation, Proc. ILWS’93, 1–15, 1993.Google Scholar
  7. [J96]
    F.V. Jensen, An Introduction to Bayesian Networks, Springer, 1996.Google Scholar
  8. [McM93]
    K.L. McMillan, Symbolic Model-Checking: an Approach to the State-Explosion problem, Kluwer, 1993.Google Scholar
  9. [MT98]
    C. Meinel and T. Theobald, Algorithms and Data Structures in VLSI Design: OBDD-Foundations and Applications, Springer, 1998.Google Scholar
  10. [P88]
    J. Pearl, Probabilistic Reasoning in Intelligent Systems, Morgan Kaufmann, 1988.Google Scholar
  11. [P94]
    M.L. Puterman, Markov Decision Processes, Wiley, 1994.Google Scholar
  12. [TP97]
    P. Tafertshofer and M. Pedram, Factored Edge-Valued Binary Decision Diagrams, Formal Methods in system Design 10, 137–164, 1997.CrossRefGoogle Scholar
  13. [VPL96]
    S. B. K. Vrudhula, M. Pedram and Y.-T. Lai, Edge-valued Binary Decision Diagrams, in T. Sasao and M. Fujita (Eds.), Representations of Discrete Functions, 109–132, Kluwer, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Marius Bozga
    • 1
  • Oded Maler
    • 1
  1. 1.Centre EquationVerimagGièeresFrance

Personalised recommendations