×

Efficient decomposition algorithm for stationary analysis of complex stochastic Petri net models. (English) Zbl 1346.68138

Kordon, Fabrice (ed.) et al., Application and theory of Petri nets and concurrency. 37th international conference, PETRI NETS 2016, Toruń, Poland, June 19–24, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-39085-7/pbk; 978-3-319-39086-4/ebook). Lecture Notes in Computer Science 9698, 281-300 (2016).
Summary: Stochastic Petri nets are widely used for the modeling and analysis of non-functional properties of critical systems. The state space explosion problem often inhibits the numerical analysis of such models. Symbolic techniques exist to explore the discrete behavior of even complex models, while block Kronecker decomposition provides memory-efficient representation of the stochastic behavior. However, the combination of these techniques into a stochastic analysis approach is not straightforward. In this paper we integrate saturation-based symbolic techniques and decomposition-based stochastic analysis methods. Saturation-based exploration is used to build the state space representation and a new algorithm is introduced to efficiently build block Kronecker matrix representation to be used by the stochastic analysis algorithms. Measurements confirm that the presented combination of the two representations can expand the limits of previous approaches.
For the entire collection see [Zbl 1337.68013].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

PRISM; SMART_
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ajmone Marsan, M.: Stochastic Petri nets: an elementary introduction. In: Rozenberg, G. (ed.) Advances in Petri Nets 1989, Covers the 9th European Workshop on Applications and Theory in Petri Nets, held in Venice, Italy in June 1988, Selected Paper. LNCS, vol. 424, pp. 1–29. Springer, Heidelberg (1988)
[2] Baier, C., Katoen, J.P., Hermanns, H.: Approximative symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR, 1999 Concurrency Theory. LNCS, vol. 1664, pp. 146–161. Springer, Heidelberg (1999) · Zbl 0934.03044 · doi:10.1007/3-540-48320-9_12
[3] Barrett, R., Berry, M.W., Chan, T.F., Demmel, J., Donato, J., Dongarra, J., Eijkhout, V., Pozo, R., Romine, C., Van der Vorst, H.: Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods, vol. 43. SIAM, Philadelphia (1994) · Zbl 0814.65030 · doi:10.1137/1.9781611971538
[4] Bause, F., Buchholz, P., Kemper, P.: A toolbox for functional and quantitative analysis of DEDS. In: Puigjaner, R., Savino, N.N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, p. 356. Springer, Heidelberg (1998) · doi:10.1007/3-540-68061-6_32
[5] Benoit, A., Plateau, B., Stewart, W.J.: Memory-efficient Kronecker algorithms with applications to the modelling of parallel systems. Future Gener. Comp. Syst. 22(7), 838–847 (2006) · doi:10.1016/j.future.2006.02.006
[6] Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995) · Zbl 1354.68167 · doi:10.1007/3-540-60692-0_70
[7] Buchholz, P.: Hierarchical structuring of superposed GSPNs. IEEE Trans. Softw. Eng. 25(2), 166–181 (1999) · Zbl 05113396 · doi:10.1109/32.761443
[8] Buchholz, P., Ciardo, G., Donatelli, S., Kemper, P.: Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comput. 12(3), 203–222 (2000) · Zbl 1040.65504 · doi:10.1287/ijoc.12.3.203.12634
[9] Buchholz, P., Kemper, P.: On generating a hierarchy for GSPN analysis. SIGMETRICS Perform. Eval. Rev. 26(2), 5–14 (1998) · Zbl 05443134 · doi:10.1145/288197.288202
[10] Buchholz, P., Kemper, P.: Kronecker based matrix representations for large Markov models. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems: A Guide to Current Research. LNCS, vol. 2925, pp. 256–295. Springer, Heidelberg (2004) · Zbl 1203.68116 · doi:10.1007/978-3-540-24611-4_8
[11] Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 78–97. Springer, Heidelberg (2003) · doi:10.1007/978-3-540-45232-4_6
[12] Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: The 8th International Workshop on Petri Nets and Performance Models, 1999, pp. 22–31. IEEE (1999) · doi:10.1109/PNPM.1999.796529
[13] Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a Petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 51–95. Springer, Heidelberg (2012) · Zbl 1350.68199 · doi:10.1007/978-3-642-29072-5_3
[14] Czekster, R.M., Rose, C., Fernandes, P.H.L., de Lima, A.M., Webber, T.: Kronecker descriptor partitioning for parallel algorithms. In: McGraw, R.M., Imsand, E.S., Chinni, M.J. (eds.) Proceedings of the 2010 Spring Simulation Multiconference, SpringSim 2010, Orlando, Florida, USA, 11–15, April 2010, p. 242. SCS/ACM (2010) · doi:10.1145/1878537.1878789
[15] Donatelli, S.: Superposed generalized stochastic Petri nets: Definition and efficient solution. In: Valette, R. (ed.) Application and Theory of Petri Nets 1994. LNCS, vol. 815, pp. 258–277. Springer, Heidelberg (1994) · doi:10.1007/3-540-58152-9_15
[16] Fernandes, P., Presotto, R., Sales, A., Webber, T.: An alternative algorithm to multiply a vector by a Kronecker represented descriptor. In: 21st UK Performance Engineering Workshop, pp. 57–67 (2005)
[17] Ghosh, R.: Scalable stochastic models for cloud services. Ph.D. thesis, Duke University (2012)
[18] Kemper, P.: Numerical analysis of superposed GSPNs. IEEE Trans. Softw. Eng. 22(9), 615–628 (1996) · Zbl 05114421 · doi:10.1109/32.541433
[19] Kwiatkowska, M., Mehmood, R., Norman, G., Parker, D.: A symbolic out-of-core solution method for Markov models. Electron. Notes Theoret. Comput. Sci. 68(4), 589–604 (2002) · Zbl 1270.68232 · doi:10.1016/S1571-0661(05)80394-9
[20] Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Int. J. Softw. Tools Technol. Transfer 6(2), 128–142 (2004) · Zbl 02243237 · doi:10.1007/s10009-004-0140-2
[21] Miner, A.S.: Efficient solution of GSPNs using canonical matrix diagrams. In: 9th International Workshop on Petri Nets and Performance Models, 2001, pp. 101–110. IEEE (2001) · doi:10.1109/PNPM.2001.953360
[22] Roux, P., Siminiceanu, R.: Model checking with edge-valued decision diagrams. In: Muñoz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, 13–15 April 2010. Proceedings. NASA Conference Proceedings, vol. NASA/CP-2010-216215, pp. 222–226 (2010)
[23] Stewart, W.J.: Probability, Markov Chains, Queues, and Simulation: The Mathematical Basis of Performance Modeling. Princeton University Press, Princeton (2009) · Zbl 1176.60003
[24] Van der Vorst, H.A.: Bi-CGSTAB: a fast and smoothly converging variant of Bi-CG for the solution of nonsymmetric linear systems. SIAM J. Scientific Stat. Comput. 13(2), 631–644 (1992) · Zbl 0761.65023 · doi:10.1137/0913035
[25] Wan, M., Ciardo, G., Miner, A.S.: Approximate steady-state analysis of large Markov models based on the structure of their decision diagram encoding. Performance Eval. 68(5), 463–486 (2011) · Zbl 06016221 · doi:10.1016/j.peva.2011.02.005
[26] Zhao, Y., Ciardo, G.: A two-phase Gauss-Seidel algorithm for the stationary solution of EVMDD-encoded CTMCs. In: Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, United Kingdom, 17–20 September 2012, pp. 74–83. IEEE Computer Society (2012) · doi:10.1109/QEST.2012.34
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.