Proportional lumpability and proportional bisimilarity. (English) Zbl 07528110
Summary: In this paper, we deal with the lumpability approach to cope with the state space explosion problem inherent to the computation of the stationary performance indices of large stochastic models. The lumpability method is based on a state aggregation technique and applies to Markov chains exhibiting some structural regularity. Moreover, it allows one to efficiently compute the exact values of the stationary performance indices when the model is actually lumpable. The notion of quasi-lumpability is based on the idea that a Markov chain can be altered by relatively small perturbations of the transition rates in such a way that the new resulting Markov chain is lumpable. In this case, only upper and lower bounds on the performance indices can be derived. Here, we introduce a novel notion of quasi-lumpability, named proportional lumpability, which extends the original definition of lumpability but, differently from the general definition of quasi-lumpability, it allows one to derive exact stationary performance indices for the original process. We then introduce the notion of proportional bisimilarity for the terms of the performance process algebra PEPA. Proportional bisimilarity induces a proportional lumpability on the underlying continuous-time Markov chains. Finally, we prove some compositionality results and show the applicability of our theory through examples.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 60J27 | Continuous-time Markov processes on discrete state spaces |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
References:
| [1] | Abate, A., Brim, L., Češka, M., Kwiatkowska, M.: Adaptive aggregation of Markov chains: Quantitative analysis of chemical reaction networks. In Proceedings of computer aided verification (CAV’15), pp. 195-213. Springer International Publishing, (2015) · Zbl 1381.68140 |
| [2] | Alzetta, G.; Marin, A.; Piazza, C.; Rossi, S., Lumping-based equivalences in Markovian automata: Algorithms and applications to product-form analyses, Inf. Comput., 260, 99-125 (2018) · Zbl 1390.68371 · doi:10.1016/j.ic.2018.04.002 |
| [3] | Baarir, S., Beccuti, M., Dutheillet, C., Franceschinis, G.: From partially to fully lumped Markov chains in stochastic well formed Petri nets. In Proceedings of Valuetools 2009 conference, pp. 44. ACM, (2009) |
| [4] | Baarir, S.; Beccuti, M.; Dutheillet, C.; Franceschinis, G.; Haddad, S., Lumping partially symmetrical stochastic models, Perform. Eval., 68, 1, 21-44 (2011) · doi:10.1016/j.peva.2010.09.002 |
| [5] | Baarir, S., Dutheillet, C., Haddad, S., Iliè, J.-M.: On the use of exact lumping in partially symmetrical Well-formed Petri Nets. In Proceedings of International Conference on the Quantitative Evaluation of Systems (QEST’05), pp. 23-32, Torino, Italy. IEEE Comp. Soc (2005) |
| [6] | Baier, C.; Katoen, J-P; Hermanns, H.; Wolf, V., Comparative branching-time semantics for Markov chains, Inf. Comput., 200, 2, 149-214 (2005) · Zbl 1101.68053 · doi:10.1016/j.ic.2005.03.001 |
| [7] | Balsamo, S., Marin, A.: Queueing Networks in Formal methods for performance evaluation, chapter 2, pp. 34-82. M. Bernardo and J. Hillston (Eds), LNCS, Springer, (2007) · Zbl 1323.68047 |
| [8] | Balsamo, Simonetta, Marin, Andrea: Product-form solutions for models with joint-state dependent transition rates. In Analytical and Stochastic Modeling Techniques and Applications, 17th International Conference, ASMTA 2010, volume 6148 of Lecture Notes in Computer Science, pp. 87-101, (2010) |
| [9] | Bernardo, M.: Weak Markovian bisimulation congruences and exact CTMC-level aggregations for concurrent processes. In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QALP’12), pp. 122-136. EPTCS, (2012) · Zbl 1458.68129 |
| [10] | Bernardo, M.: Weak Markovian bisimulation congruences and exact CTMC-level aggregations for sequential processes. In Proceedings of the 6th international conference on trustworthy global computing (TGC’11), volume 7173 of LNCS, pp. 89-103. Springer, (2012) · Zbl 1458.68129 |
| [11] | Bernardo, M., On the tradeoff between compositionality and exactness in weak bisimilarity for integrated-time markovian process calculi, Theor. Comput. Sci., 563, 99-143 (2015) · Zbl 1302.68199 · doi:10.1016/j.tcs.2014.10.025 |
| [12] | Bravetti, M., Revisiting interactive Markov chains, Electr. Notes Theor. Comput. Sci., 68, 5, 65-84 (2003) · Zbl 1270.68207 · doi:10.1016/S1571-0661(04)80520-6 |
| [13] | Buchholz, P., Exact and ordinary lumpability in finite Markov chains, J. Appl. Probab., 31, 59-75 (1994) · Zbl 0796.60073 · doi:10.2307/3215235 |
| [14] | Cardelli, L.; Tribastone, M.; Tschaikowski, M.; Vandin, A., Symbolic computation of differential equivalences, Theoret. Comput. Sci., 777, 132-154 (2019) · Zbl 1425.68463 · doi:10.1016/j.tcs.2019.03.018 |
| [15] | Coleman, JL; Henderson, W.; Taylor, PG, Product form equilibrium distributions and a convolution algorithm for Stochastic Petri nets, Perf. Eval., 26, 3, 159-180 (1996) · Zbl 0900.68321 · doi:10.1016/0166-5316(95)00023-2 |
| [16] | Daly, D., Buchholz, P., Sanders, W.H.: Bound-preserving composition for markov reward models. In Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), pp. 243-252, (2006) |
| [17] | Derisavi, S.; Hermanns, H.; Sanders, WH, Optimal state-space lumping in Markov chains, Elsevier Inform. Process. Lett., 87, 6, 309-315 (2003) · Zbl 1189.68039 · doi:10.1016/S0020-0190(03)00343-0 |
| [18] | Franceschinis, G.; Muntz, R., Bounds for quasi-lumpable Markov chains, Perform. Eval., 20, 1-3, 223-243 (1994) · doi:10.1016/0166-5316(94)90015-9 |
| [19] | Franceschinis, G.; Muntz, R., Computing bounds for the performance indices of quasi-lumpable stochastic well-formed nets, IEEE Trans. Softw. Eng., 20, 7, 516-525 (1994) · Zbl 0938.68521 · doi:10.1109/32.297940 |
| [20] | Hermanns, H., Interactive Markov Chains (2002), New York: Springer, New York · Zbl 1012.68142 · doi:10.1007/3-540-45804-2 |
| [21] | Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge Press, (1996) · Zbl 1080.68003 |
| [22] | Kemeny, JG; Snell, JL, Finite Markov Chains (1976), New York: Springer, New York · Zbl 0328.60035 |
| [23] | Kuo, JCW; Wei, J., Lumping analysis in monomolecular reaction systems. analysis of approximately lumpable system., Ind. Eng. Chem. Fund., 8, 1, 124-133 (1969) · doi:10.1021/i160029a020 |
| [24] | Ledoux, J., A necessary condition for weak lumpability in finite Markov processes, Oper. Res. Lett., 13, 3, 165-168 (1993) · Zbl 0780.90108 · doi:10.1016/0167-6377(93)90006-3 |
| [25] | Li, G.; Rabitz, H., A general analysis of exact lumping in chemical kinetics, Chem. Eng. Sci., 44, 6, 1413-1430 (1989) · doi:10.1016/0009-2509(89)85014-6 |
| [26] | Marin, A., Piazza, C., Rossi, S.: Proportional lumpability. In Formal modeling and analysis of timed systems—17th international conference, formats 2019, proceedings, volume 11750 of lecture notes in computer science, pp. 265-281. Springer, (2019) · Zbl 1434.68055 |
| [27] | Marin, A., Rossi, S.: Autoreversibility: exploiting symmetries in Markov chains. In Proceedings of IEEE MASCOTS, pages 151-160, san Francisco, CA, USA (2013) |
| [28] | Marin, A.; Rossi, S., On the relations between Markov chain lumpability and reversibility, Acta Inform., 54, 5, 447-485 (2017) · Zbl 1398.60085 · doi:10.1007/s00236-016-0266-1 |
| [29] | Milios, D.; Gilmore, S., Component aggregation for PEPA models: An approach based on approximate strong equivalence, Perform. Eval., 94, 43-71 (2015) · doi:10.1016/j.peva.2015.09.004 |
| [30] | Molloy, MK, Performance analysis using stochastic petri nets, IEEE Trans. Comput., 31, 9, 913-917 (1982) · doi:10.1109/TC.1982.1676110 |
| [31] | Plateau, B., On the stochastic structure of parallelism and synchronization models for distributed algorithms, SIGMETRICS Perf. Eval. Rev., 13, 2, 147-154 (1985) · doi:10.1145/317786.317819 |
| [32] | Smith, M.J.A.: Compositional abstractions for long-run properties of stochastic systems. In: Eighth international conference on quantitative evaluation of systems, QEST 2011, 223-232 (2011) |
| [33] | Sumita, U.; Rieders, M., Lumpability and time-reversibility in the aggregation-disaggregation method for large Markov chains, Commun. Stat. Stoch. Models, 5, 63-81 (1989) · Zbl 0667.60068 · doi:10.1080/15326348908807099 |
| [34] | Thomas, Nigel, Harrison, Peter G.: Semi-product-form solution for PEPA models with functional rates. In Analytical and Stochastic Modelling Techniques and Applications - 20th International Conference, ASMTA 2013, volume 7984 of Lecture Notes in Computer Science, pages 416-430, (2013) · Zbl 1390.68492 |
| [35] | Tomlin, AS; Li, G.; Rabitz, H.; Tóth, J., The effect of lumping and expanding on kinetic differential equations., SIAM J. Appl. Math., 57, 6, 1531-1556 (1997) · Zbl 0891.34030 · doi:10.1137/S0036139995293294 |
| [36] | Towsley, DF, Queuing network models with state-dependent routing, J. ACM, 27, 2, 323-337 (1980) · Zbl 0441.68037 · doi:10.1145/322186.322196 |
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.
