Skip to main content
SpringerLink
Log in

Symbolic Representations and Analysis of Large Probabilistic Systems

  • Chapter
Validation of Stochastic Systems

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2925))

Abstract

This paper describes symbolic techniques for the construction, representation and analysis of large, probabilistic systems. Symbolic approaches derive their efficiency by exploiting high-level structure and regularity in the models to which they are applied, increasing the size of the state spaces which can be tackled. In general, this is done by using data structures which provide compact storage but which are still efficient to manipulate, usually based on binary decision diagrams (BDDs) or their extensions. In this paper we focus on BDDs, multi-valued decision diagrams (MDDs), multi-terminal binary decision diagrams (MTBDDs) and matrix diagrams.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. PRISM web site, www.cs.bham.ac.uk/~dxp/prism

  2. SMART web site, http://www.cs.wm.edu/~ciardo/SMART/

  3. Akers, S.: Binary decision diagrams. IEEE Transactions on Computers C-27(6), 509–516 (1978)

    Article  Google Scholar 

  4. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)

    Google Scholar 

  5. Bahar, I., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In Proc. International Conference on Computer-Aided Design (ICCAD 1993), pp. 188–191 (1993); Also available in Formal Methods in System Design 10(2/3), 171–206 (1997)

    Google Scholar 

  6. Baier, C.: On algorithmic verification methods for probabilistic systems. In: Habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim (1998)

    Google Scholar 

  7. Baier, C., Clarke, E.: The algebraic mu-calculus and MTBDDs. In: Proc. 5th Workshop on Logic, Language, Information and Computation (WOLLIC 1998), pp. 27–38 (1998)

    Google Scholar 

  8. Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430–440. Springer, Heidelberg (1997)

    Google Scholar 

  9. Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time markov chains (Extended abstract). In: Baeten, J., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–161. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  10. Bollig, B., Wegner, I.: Improving the variable ordering of OBDDs is NPcomplete. IEEE Transactions on Computers 45(9), 993–1006 (1996)

    Article  MATH  Google Scholar 

  11. Bozga, M., Maler, O.: On the representation of probabilities over structured domains. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 261–273. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Brace, K., Rudell, R., Bryant, R.: Efficient implementation of a BDD package. In: Proc. 27th Design Automation Conference (DAC 1990), pp. 40–45. IEEE Computer Society Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  13. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  14. Bryant, R.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)

    Article  Google Scholar 

  15. Buchholz, P., Ciardo, G., Donatelli, S., Kemper, P.: Complexity of memoryefficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp.( SUMMER 2000) 12(3), 203–222 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  16. Buchholz, P., Kemper, P.: Numerical analysis of stochastic marked graphs. In: 6th Int. Workshop on Petri Nets and Performance Models (PNPM 1995), Durham, NC, October 1995, pp. 32–41. IEEE Comp. Soc. Press, Los Alamitos (1995)

    Chapter  Google Scholar 

  17. Buchholz, P., Kemper, P.: Compact representations of probability distributions in the analysis of superposed GSPNs. In: German, R., Haverkort, B. (eds.) Proc. 9th International Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 81–90. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  18. Buchholz, P., Kemper, P.: Kronecker based matrix representations for large Markov models. In: This proceedings (2003)

    Google Scholar 

  19. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. In: Proc. 5th Annual IEEE Symposium on Logic in Computer Science (LICS 1990), pp. 428–439. IEEE Computer Society Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  20. Ciardo, G., Luettgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  21. Ciardo, G., Luettgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Ciardo, G., Miner, A.: SMART: Simulation and Markovian analyser for reliability and timing. In: Proc. 2nd International Computer Performance and Dependability Symposium (IPDS1996), p. 60. IEEE Computer Society Press, Los Alamitos (1996)

    Chapter  Google Scholar 

  23. Ciardo, G., Miner, A.: Storage alternatives for large structured state spaces. In: Marie, R., Plateau, B., Calzarossa, M., Rubino, G. (eds.) TOOLS 1997. LNCS, vol. 1245, pp. 44–57. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  24. Ciardo, G., Miner, A.: A data structure for the efficient Kronecker solution of GSPNs. In: Buchholz, P., Silva, M. (eds.) Proc. 8th International Workshop on Petri Nets and Performance Models (PNPM 1999), pp. 22–31. IEEE Computer Society Press, Los Alamitos (1999)

    Chapter  Google Scholar 

  25. Ciardo, G., Siminiceanu, R.: Using edge-valued decision diagrams for symbolic generation of shortest paths. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 256–273. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Ciesinski, F., Grössner, F.: On probabilistic computation tree logic. This proceedings (2003)

    Google Scholar 

  27. Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: Proc. International Workshop on Logic Synthesis (IWLS 1993), pp. 1–15 (1993); Also available in Formal Methods in System Design 10(2/3), 149–169 (1997)

    Google Scholar 

  28. Clarke, E., McMillan, K., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: Proc. 30th Design Automation Conference (DAC 1993), pp. 54–60. ACM Press, New York (1993); Also available in Formal Methods in System Design 10(2/3), 137–148 (1997)

    Google Scholar 

  29. Cloth, L.: Specification and verification of Markov reward models. In: This proceedings (2003)

    Google Scholar 

  30. Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 365–373. Springer, Heidelberg (1989)

    Google Scholar 

  31. D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  32. Davies, I., Knottenbelt, W., Kritzinger, P.: Symbolic methods for the state space exploration of GSPN models. In: Field, T., Harrison, P., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 188–199. Springer, Heidelberg (2002)

    Google Scholar 

  33. Davio, M.: Kronecker products and shuffle algebra. IEEE Transactions on Computers, C 30(2), 116–125 (1981)

    MATH  MathSciNet  Google Scholar 

  34. de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using mTBDDs and the kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  35. Donatelli, S.: Superposed stochastic automata: A class of stochastic Petri nets amenable to parallel solution. Performance Evaluation 18, 21–36 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  36. Enders, R., Filkorn, T., Taubner, D.: Generating BDDs for symbolic model checking in CCS. In: Larsen, K., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 203–213. Springer, Heidelberg (1992)

    Google Scholar 

  37. Fernandes, P., Plateau, B., Stewart, W.: Efficient descriptor-vector multiplication in stochastic automata networks. Journal of the ACM 45(3), 381–414 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  38. Fujita, M., Matsunaga, Y., Kakuda, T.: On the variable ordering of binary decision diagrams for the application of multi-level synthesis. In: European conference on Design automation, pp. 50–54 (1991)

    Google Scholar 

  39. Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Probabilistic analysis of large finite state machines. In: Proc. 31st Design Automation Conference (DAC 1994), pp. 270–275. ACM Press, New York (1994)

    Chapter  Google Scholar 

  40. Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Markovian analysis of large finite state machines. IEEE Trans. on CAD 15(12), 1479–1493 (1996)

    Google Scholar 

  41. Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects of Computing 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  42. Hartonas-Garmhausen, V.: Probabilistic Symbolic Model Checking with Engineering Models and Applications. PhD thesis, Carnegie Mellon University (1998)

    Google Scholar 

  43. Hermanns, H., Kwiatkowska, M., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems 56(1-2), 23–67 (2003)

    MATH  MathSciNet  Google Scholar 

  44. Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188–207. Prensas Universitarias de Zaragoza (1999)

    Google Scholar 

  45. Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 244–264. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  46. Hillston, J., Kloul, L.: An efficient Kronecker representation for PEPA models. In: Proc. Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV 2001), pp. 120–135. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  47. Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1–2), 9–62 (1998)

    MATH  MathSciNet  Google Scholar 

  48. Katoen, J.-P., Kwiatkowska, M., Norman, G., Parker, D.: Faster and symbolic CTMC model checking. In: de Alfaro, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 23–38. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  49. Kuntz, M., Siegle, M.: Deriving symbolic representations from stochastic process algebras. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 188–206. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  50. Kwiatkowska, M., Mehmood, R., Norman, G., Parker, D.: A symbolic out-of-core solution method for Markov models. In: Proc. Workshop on Parallel and Distributed Model Checking (PDMC 2002). Electronic Notes in Theoretical Computer Science, vol. 68.4. Elsevier, Amsterdam (2002)

    Google Scholar 

  51. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)

    Google Scholar 

  52. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52–66. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  53. Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex. Technical Report CSR-99-1, School of Computer Science, University of Birmingham (1999)

    Google Scholar 

  54. Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194–206. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  55. Lee, C.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal 38, 985–999 (1959)

    MathSciNet  Google Scholar 

  56. McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  57. Miner, A.: Data Structures for the Analysis of Large Structured Markov Chains. PhD thesis, Department of Computer Science, College of William & Mary, Virginia (2000)

    Google Scholar 

  58. Miner, A.: Efficient solution of GSPNs using canonical matrix diagrams. In: German, R., Haverkort, B. (eds.) Proc. 9th International Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 101–110. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  59. Miner, A.: Efficient state space generation of GSPNs using decision diagrams. In: Proc. 2002 Int. Conf. on Dependable Systems and Networks (DSN 2002), Washington, DC, June 2002, pp. 637–646 (2002)

    Google Scholar 

  60. Miner, A., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6–25. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  61. Miner, A., Ciardo, G., Donatelli, S.: Using the exact state space of a Markov model to compute approximate stationary measures. In: Proc. 2000 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, Santa Clara, CA, June 2000, pp. 207–216 (2000)

    Google Scholar 

  62. Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)

    Google Scholar 

  63. Pastor, E., Cortadella, J.: Efficient encoding schemes for symbolic analysis of Petri nets. In: Design Automation and Test in Europe (DATE 1998), Paris (February 1998)

    Google Scholar 

  64. Pastor, E., Cortadella, J., Peña, M.: Structural methods to improve the symbolic analysis of Petri nets. In: 20th International Conference on Application and Theory of Petri Nets, Williamsburg (June 1999)

    Google Scholar 

  65. Plateau, B.: 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, Performance Evaluation Review, vol. 13(2), pp. 147–153 (1985)

    Google Scholar 

  66. Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proc. International Conference on Computer-Aided Design (ICCAD 1993), pp. 42–47 (1993)

    Google Scholar 

  67. Siegle, M.: Compositional representation and reduction of stochastic labelled transition systems based on decision node BDDs. In: Baum, D., Mueller, N., Roedler, R. (eds.) Proc. Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen (MMB 1999), pp. 173–185. VDE Verlag (1999)

    Google Scholar 

  68. Siegle, M.: Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Habilitation thesis, Universität Erlangen-Nürnberg (2002)

    Google Scholar 

  69. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains, Princeton (1994)

    Google Scholar 

  70. Xie, A., Beerel, A.: Symbolic techniques for performance analysis of timed circuits based on average time separation of events. In: Proc. 3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 1997), pp. 64–75. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  71. Zampunièris, D.: The Sharing Tree Data Structure, Theory and Applications in Formal Verification. PhD thesis, Department of Computer Science, University of Namur, Belgium (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, Iowa State University, Ames, Iowa, 50011

    Andrew Miner

  2. School of Computer Science, University of Birmingham, UK

    David Parker

Authors
  1. Andrew Miner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Parker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Theoretical Computer Science, Technical University Dresden, Germany

    Christel Baier

  2. Centre for Telematics and Information Technology, Faculty for Electrical Engineering, Mathematics and Computer Science, University of Twente, P.O. Box 217, 7500, AE, Netherlands

    Boudewijn R. Haverkort

  3. VASY, INRIA, Grenoble Rhône-Alpes, France

    Holger Hermanns

  4. Software Modeling and Verification, RWTH Aachen University, Germany

    Joost-Pieter Katoen

  5. Institut für Technische Informatik, Universität der Bundeswehr München,  

    Markus Siegle

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Miner, A., Parker, D. (2004). Symbolic Representations and Analysis of Large Probabilistic Systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, JP., Siegle, M. (eds) Validation of Stochastic Systems. Lecture Notes in Computer Science, vol 2925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24611-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24611-4_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22265-1

  • Online ISBN: 978-3-540-24611-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation