Advertisement

Explicit State Space and Markov Chain Generation Using Decision Diagrams

  • Junaid Babar
  • Andrew S. Miner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8721)

Abstract

Various forms of decision diagrams have been successfully used for quite some time to generate the state space and Markov chain from models expressed in some high-level formalism. A variety of efficient, “symbolic” algorithms, which manipulate sets of states instead of individual states, are known for this purpose. However, there are cases where explicit generation algorithms are still used. This paper seeks to efficiently use decision diagrams as replacement data structures within an existing explicit generation implementation. The necessary decision diagram algorithms are presented, and small changes to the explicit generation algorithm are suggested to improve the overall generation process. The efficiency of the new algorithms is illustrated using several models.

Keywords

Quantitative model checking Markov chain generation Markov chain storage decision diagrams 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Babar, J., Beccuti, M., Donatelli, S., Miner, A.: GreatSPN enhanced with decision diagram data structures. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 308–317. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  2. 2.
    Babar, J., Miner, A.: Meddly: Multi–terminal and Edge–valued Decision Diagram LibrarY. In: 7th Int. Conf. on Quantitative Evaluation of Systems (QEST 2010), pp. 195–196 (September 2010)Google Scholar
  3. 3.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)CrossRefGoogle Scholar
  4. 4.
    Bryant, R.E.: Graph–based algorithms for boolean function manipulation. IEEE Trans. Comp. C-35(8), 677–691 (1986)Google Scholar
  5. 5.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Chiola, G., Franceschinis, G., Gaeta, R., Ribaudo, M.: GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets. Perf. Eval. 24(1-2), 47–68 (1995)CrossRefzbMATHGoogle Scholar
  7. 7.
    Chiola, G.: Compiling techniques for the analysis of stochastic Petri nets. In: Proc. 4th Int. Conf. on Modelling Techniques and Tools for Performance Evaluation, pp. 13–27 (1989)Google Scholar
  8. 8.
    Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed colored nets and symmetric modeling applications. IEEE Trans. Comp. 42(11), 1343–1360 (1993)CrossRefGoogle Scholar
  9. 9.
    Ciardo, G., Lüttgen, G., Miner, A.S.: Exploiting interleaving semantics in symbolic state–space generation. Formal Methods in System Design 31(1), 63–100 (2007)CrossRefzbMATHGoogle Scholar
  10. 10.
    PCiardo, G., Miner, A.S., Wan, M.: Advanced features in SMART: the Stochastic Model checking Analyzer for Reliability and Timing. SIGMETRICS Perform. Eval. Rev. 36(4), 58–63 (2009)CrossRefGoogle Scholar
  11. 11.
    Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval. 18(1), 37–59 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443–457. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Delamare, C., Gardan, Y., Moreaux, P.: Performance evaluation with asynchronously decomposable SWN: Implementation and case study. In: 10th Int. Workshop on Petri Nets and Performance Models (PNPM 2003), pp. 20–29. IEEE Comp. Soc. Press (September 2003)Google Scholar
  14. 14.
    Derisavi, S.: A symbolic algorithm for optimal Markov chain lumping. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 139–154. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    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)CrossRefzbMATHMathSciNetGoogle Scholar
  16. 16.
    Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi–valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1-2), 9–62 (1998)zbMATHMathSciNetGoogle Scholar
  17. 17.
    Lai, Y.T., Pedram, M., Vrudhula, S.B.K.: Formal verification using edge–valued binary decision diagrams. IEEE Trans. Comp. 45, 247–255 (1996)CrossRefzbMATHGoogle Scholar
  18. 18.
    Miner, A., Parker, D.: Symbolic representations and analysis of large state spaces. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) AUTONOMY 2003. LNCS (LNAI), vol. 2925, pp. 296–338. Springer, Heidelberg (2004)Google Scholar
  19. 19.
    Miner, A.S.: Efficient solution of GSPNs using Canonical Matrix Diagrams. In: 9th Int. Workshop on Petri Nets and Performance Models (PNPM 2001), pp. 101–110. IEEE Comp. Soc. Press (September 2001)Google Scholar
  20. 20.
    Miner, A.S.: Implicit GSPN reachability set generation using decision diagrams. Perf. Eval. 56(1-4), 145–165 (2004)CrossRefGoogle Scholar
  21. 21.
    Model Checking Contest at Petri Nets (2014), http://mcc.lip6.fr/models.php
  22. 22.
    Molloy, M.K.: Performance analysis using stochastic Petri nets. IEEE Trans. Comp. 31(9), 913–917 (1982)CrossRefGoogle Scholar
  23. 23.
    Muppala, J.K., Ciardo, G., Trivedi, K.S.: Modeling using Stochastic Reward Nets. In: Proc. 1st Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 1993), pp. 367–372. IEEE Comp. Soc. Press, San Diego (1993)Google Scholar
  24. 24.
    Pastor, E., Roig, O., Cortadella, J., Badia, R.M.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  25. 25.
    Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: 1st International Workshop on Manufacturing and Petri Nets, Osaka, Japan, pp. 215–234 (June 1996)Google Scholar
  26. 26.
    Wan, M., Ciardo, G., Miner, A.S.: Approximate steady–state analysis of large Markov models based on the structure of their decision diagram encoding. Perf. Eval. 68(5), 463–486 (2011)CrossRefGoogle Scholar
  27. 27.
    Wimmer, R., Braitling, B., Becker, B., Hahn, E.M., Crouzen, P., Hermanns, H., Dhama, A., Theel, O.: Symblicit calculation of long–run averages for concurrent probabilistic systems. In: 7th Int. Conf. on Quantitative Evaluation of Systems (QEST 2010), pp. 27–36 (2010)Google Scholar
  28. 28.
    Woodside, C.M., Li, Y.: Performance Petri net analysis of communications protocol software by delay-equivalent aggregation. In: 4th Int. Workshop on Petri Nets and Performance Models (PNPM 1991), pp. 64–73. IEEE Comp. Soc. Press, Melbourne (1991)Google Scholar
  29. 29.
    Xie, A., Beerel, P.A.: Efficient state classification of finite state Markov chains. IEEE Trans. Computer-Aided Design 17(12), 1334–1339 (1998)CrossRefGoogle Scholar
  30. 30.
    Yoneda, T., Hatori, H., Takahara, A., Minato, S.: BDDs vs. zero–suppressed BDDs: for CTL symbolic model checking of Petri nets. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 435–449. Springer, Heidelberg (1996)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Junaid Babar
    • 1
  • Andrew S. Miner
    • 1
  1. 1.Department of Computer ScienceIowa State UniversityAmesUSA

Personalised recommendations