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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
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)
Bryant, R.E.: Graph–based algorithms for boolean function manipulation. IEEE Trans. Comp. C-35(8), 677–691 (1986)
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)
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)
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)
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)
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)
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)
Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval. 18(1), 37–59 (1993)
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)
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)
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)
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)
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)
Lai, Y.T., Pedram, M., Vrudhula, S.B.K.: Formal verification using edge–valued binary decision diagrams. IEEE Trans. Comp. 45, 247–255 (1996)
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)
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)
Miner, A.S.: Implicit GSPN reachability set generation using decision diagrams. Perf. Eval. 56(1-4), 145–165 (2004)
Model Checking Contest at Petri Nets (2014), http://mcc.lip6.fr/models.php
Molloy, M.K.: Performance analysis using stochastic Petri nets. IEEE Trans. Comp. 31(9), 913–917 (1982)
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)
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)
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)
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)
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)
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)
Xie, A., Beerel, P.A.: Efficient state classification of finite state Markov chains. IEEE Trans. Computer-Aided Design 17(12), 1334–1339 (1998)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Babar, J., Miner, A.S. (2014). Explicit State Space and Markov Chain Generation Using Decision Diagrams. In: Horváth, A., Wolter, K. (eds) Computer Performance Engineering. EPEW 2014. Lecture Notes in Computer Science, vol 8721. Springer, Cham. https://doi.org/10.1007/978-3-319-10885-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-10885-8_17
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10884-1
Online ISBN: 978-3-319-10885-8
eBook Packages: Computer ScienceComputer Science (R0)