# zbMATH — the first resource for mathematics

Lumping-based equivalences in Markovian automata: algorithms and applications to product-form analyses. (English) Zbl 1390.68371
Summary: In this paper we consider two relations over stochastic automata, named lumpable bisimulation and exact equivalence, that induce a strong and an exact lumping, respectively, on the underlying Markov chains. We show that an exact equivalence over the states of a non-synchronising automaton is indeed a lumpable bisimulation for the corresponding reversed automaton and then it induces a strong lumping on the time-reversed Markov chain underlying the model. This property allows us to prove that the class of quasi-reversible models is closed under exact equivalence. Quasi-reversibility is a pivotal property to study product-form models. Hence, exact equivalence turns out to be a theoretical tool to prove the product-form of models by showing that they are exactly equivalent to models which are known to be quasi-reversible. Algorithms for computing both lumpable bisimulation and exact equivalence are introduced. Case studies as well as performance tests are also presented.

##### MSC:
 68Q45 Formal languages and automata 68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
##### Software:
 [1] Baarir, S.; Beccuti, M.; Dutheillet, C.; Franceschinis, G.; Haddad, S., Lumping partially symmetrical stochastic models, Perform. Eval., 68, 1, 21-44, (2011) [2] Baier, C.; Katoen, J.-P.; Hermanns, H., Comparative branching-time semantics for Markov chains, Inf. Comput., 200, 2, 149-214, (2005) · Zbl 1101.68053 [3] Balsamo, S.; De Nitto Persone’, V.; Onvural, R., Analysis of queueing networks with blocking, (2001), Kluwer Academic Publishers · Zbl 0977.68007 [4] S. Balsamo, P.G. Harrison, A. Marin, A unifying approach to product-forms in networks with finite capacity constraints, in: Vishal Misra, Paul Barford, Mark S. Squillante (Eds.), Proc. of the 2010 ACM SIGMETRICS Int. Conf. on Measurement and Modeling of Computer Systems, New York, NY, USA, 14-18 June 2010, pp. 25-36. [5] Balsamo, S.; Marin, A., Queueing networks, (Bernardo, M.; Hillston, J., Formal Methods for Performance Evaluation, Lect. Notes Comput. Sci., (2007), Springer), 34-82, (chapter 2) · Zbl 1323.68047 [6] Balsamo, S.; Dei Rossi, G.; Marin, A., Lumping and reversed processes in cooperating automata, Ann. Oper. Res., 239, 2, 695-722, (2014) · Zbl 1342.60130 [7] Baskett, F.; Chandy, K. M.; Muntz, R. R.; Palacios, F. G., Open, closed, and mixed networks of queues with different classes of customers, J. ACM, 22, 2, 248-260, (1975) · Zbl 0313.68055 [8] Bernardo, M.; Gorrieri, R., A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time, Theor. Comput. Sci., 202, 1-54, (1998) · Zbl 0902.68075 [9] Bradley, J. T.; Dingle, N. J.; Gilmore, S. T.; Knottenbelt, W. J., Derivation of passage-time densities in PEPA models using ipc: the imperial PEPA compiler, (Proc. of the 11th International Symposium on Modelling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS’03, (2003)), 344-351 [10] Buchholz, P., Exact and ordinary lumpability in finite Markov chains, J. Appl. Probab., 31, 59-75, (1994) · Zbl 0796.60073 [11] Buchholz, P., Exact performance equivalence: an equivalence relation for stochastic automata, Theor. Comput. Sci., 215, 1-2, 263-287, (1999) · Zbl 0913.68141 [12] Bugliesi, M.; Gallina, L.; Hamadou, S.; Marin, A.; Rossi, S., Behavioural equivalences and interference metrics for mobile ad-hoc networks, Perform. Eval., 73, 41-72, (2014) [13] Gelenbe, E.; Fourneau, J. M., Flow equivalence and stochastic equivalence in G-networks, Comput. Manag. Sci., 1, 2, 179-192, (2004) · Zbl 1115.90319 [14] Harrison, P. G., Turning back time in Markovian process algebra, Theor. Comput. Sci., 290, 3, 1947-1986, (2003) · Zbl 1044.68117 [15] Harrison, P. G.; Marin, A., Product-forms in multi-way synchronizations, Comput. J., 57, 11, 1693-1710, (2014) [16] Hermanns, H., Interactive Markov chains, (2002), Springer · Zbl 1012.68142 [17] Hermanns, H.; Herzog, U.; Katoen, J. P., Process algebra for performance evaluation, Theor. Comput. Sci., 274, 1-2, 43-87, (2002) · Zbl 0992.68149 [18] Hillston, J., A compositional approach to performance modelling, (1996), Cambridge Press [19] Hillston, J.; Marin, A.; Piazza, C.; Rossi, S., Contextual lumpability, (Proc. of the 7th International Conference on Performance Evaluation Methodologies and Tools, Valuetools’13, (2013), ACM Press), 194-203 [20] Kelly, F., Reversibility and stochastic networks, (1979), Wiley New York · Zbl 0422.60001 [21] Kemeny, J. G.; Snell, J. L., Finite Markov chains, (1976), Springer · Zbl 0328.60035 [22] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inf. Comput., 94, 1, 1-28, (1991) · Zbl 0756.68035 [23] Le Boudec, J. Y., A BCMP extension to multiserver stations with concurrent classes of customers, (Proc. of the 1986 International Conference on Computer Performance Modelling, Measurement and Evaluation, ACM SIGMETRICS’86, (1986), ACM Press), 78-91 [24] Marin, A.; Rossi, S., Lumping-based equivalences in Markovian automata and applications to product-form analyses, (Proc. of the 12th International Conference on Quantitative Evaluation of SysTems, QEST’15, Lect. Notes Comput. Sci., vol. 9259, (2015), Springer), 160-175 [25] Marin, A.; Rossi, S., Aggregation and truncation of reversible Markov chains modulo state renaming, (Proc of the 24th International Conference on Analytical and Stochastic Modelling Techniques and Applications, ASMTA’17, Lect. Notes Comput. Sci., vol. 10378, (2017)), 152-165 [26] Marin, A.; Rossi, S., On the relations between Markov chain lumpability and reversibility, Acta Inform., 54, 5, 447-485, (2017) · Zbl 1398.60085 [27] Marin, A.; Rossi, Sabina, Quantitative analysis of concurrent reversible computations, (Proc. of the 13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’15, Lect. Notes Comput. Sci., vol. 9268, (2015), Springer-Verlag), 206-221 · Zbl 1465.68197 [28] Marin, A.; Vigliotti, M. G., A general result for deriving product-form solutions of Markovian models, (Proc. of First Joint WOSP/SIPEW International Conference on Performance Engineering, (2010), ACM), 165-176 [29] Molloy, M. K., Performance analysis using stochastic Petri nets, IEEE Trans. Comput., 31, 9, 913-917, (1982) [30] Paige, R.; Tarjan, R. E., Three partition refinement algorithms, SIAM J. Comput., 16, 6, 973-989, (1987) · Zbl 0654.68072 [31] Pittel, B., Closed exponential networks of queues with saturation: the Jackson-type stationary distribution and its asymptotic analysis, Math. Oper. Res., 4, 4, 357-378, (1979) · Zbl 0418.60089 [32] Plateau, B., On the stochastic structure of parallelism and synchronization models for distributed algorithms, SIGMETRICS Perform. Eval. Rev., 13, 2, 147-154, (1985) [33] Schweitzer, P., Aggregation methods for large Markov chains, (Mathematical Computer Performance and Reliability, (1984)) [34] Sproston, J.; Donatelli, S., Backward bisimulation in Markov chain model checking, IEEE Trans. Softw. Eng., 32, 8, 531-546, (2006) [35] Sumita, U.; Reiders, 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 [36] Valmari, A.; Franceschinis, G., Simple $$O(m \log n)$$ time Markov chain lumping, (Proc. of 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS’10, Lect. Notes Comput. Sci., vol. 6015, (2010)), 38-52 · Zbl 1284.68437