Performance preserving equivalence for stochastic process algebra dtsdPBC

I. V. Tarasyuk

Sibirskie èlektronnye matematičeskie izvestiâ, Tome 20 (2023) no. 2, pp. 646-699.

Résumé

Petri box calculus (PBC) of E. Best, R. Devillers, J.G. Hall and M. Koutny is a well-known algebra of parallel processes with a Petri net semantics. Discrete time stochastic and deterministic PBC (dtsdPBC) of the author extends PBC with discrete time stochastic and deterministic delays. dtsdPBC has a step operational semantics via labeled probabilistic transition systems and a Petri net denotational semantics via dtsd-boxes, a subclass of labeled discrete time stochastic and deterministic Petri nets (LDTSDPNs). To evaluate performance in dtsdPBC, the underlying semi-Markov chains (SMCs) and (reduced) discrete time Markov chains (DTMCs and RDTMCs) of the process expressions are analyzed. Step stochastic bisimulation equivalence is used in dtsdPBC as to compare the qualitative and quantitative behaviour, as to establish consistency of the operational and denotational semantics. We demonstrate how to apply step stochastic bisimulation equivalence of the process expressions for quotienting their transition systems, SMCs, DTMCs and RDTMCs while preserving the stationary behaviour and residence time properties. We also prove that the quotient behavioural structures (transition systems, reachability graphs and SMCs) of the process expressions and their dtsd-boxes are isomorphic. Since the equivalence guarantees identity of the functional and performance characteristics in the equivalence classes, it can be used to simplify performance analysis within dtsdPBC due to the quotient minimization of the state space.

Détail

Keywords: Petri box calculus, discrete time, stochastic and deterministic delays, transition system, operational semantics, dtsd-box, denotational semantics, performance, stochastic bisimulation
Mots-clés : Markov chain, quotient.

Bibliographie

[1] W.M.P. van der Aalst, K.M. van Hee, H.A. Reijers, “Analysis of discrete-time stochastic Petri nets”, Stat. Neerl., 54:2 (2000), 237–255 | DOI | MR | Zbl

[2] A. Aldini, M. Bernardo, F. Corradini, A process algebraic approach to software architecture design, Springer, London, 2010 | Zbl

[3] C. Autant, Ph. Schnoebelen, “Place bisimulations in Petri nets”, Application and Theory of Petri Nets 1992, Lect. Notes in Comput. Sci., 616, ed. Jensen K., Springer, Berlin–Heidelberg, 1992, 45–61 | DOI | MR

[4] G. Balbo, “Introduction to stochastic Petri nets”, Lectures on Formal methods and performance analysis, 1st EEF/Euro summer school on trends in computer science (Berg en Dal, the Netherlands, July 3-7, 2000), Lect. Notes in Comput. Sci., 2090, eds. Brinksma Ed et al., Springer, Berlin, 2001, 84–155 | DOI | Zbl

[5] G. Balbo, “Introduction to generalized stochastic Petri nets”, Formal methods for performance evaluation, 7th international school on formal methods for the design of computer, communication, and software systems, SFM 2007, Advanced lectures (Bertinoro, Italy, May 28 - June 2, 2007), Lect. Notes in Comput. Sci., 4486, eds. Bernardo Marco et al., Springer, Berlin, 2007, 83–131 | DOI | Zbl

[6] E. Bartocci, P. Lió, “Computational modeling, formal analysis, and tools for systems biology”, PLoS Computational Biology, 12:1 (2016), e1004591 | DOI

[7] F. Bause, P.S. Kritzinger, Stochastic Petri nets. An introduction to the theory, Vieweg Verlag, Wiesbaden, 2002 | Zbl

[8] J.A. Bergstra, J.W. Klop, “Algebra of communicating processes with abstraction”, Theor. Comput. Sci., 37:1 (1985), 77–121 | DOI | MR | Zbl

[9] M. Bernardo, Theory and application of extended Markovian process algebra, Ph.D. thesis, University of Bologna, Italy, 1999

[10] M. Bernardo, “A survey of Markovian behavioral equivalences”, Formal methods for performance evaluation, Lect. Notes in Comput. Sci., 4486, eds. Bernardo Marco et al., Springer, Berlin, 2007, 180–219 | DOI | Zbl

[11] M. Bernardo, “Non-bisimulation-based Markovian behavioral equivalences”, J. Log. Algebr. Program., 72:1 (2007), 3–49 | DOI | MR | Zbl

[12] M. Bernardo, “On the tradeoff between compositionality and exactness in weak bisimilarity for integrated-time Markovian process calculi”, Theoret. Comput. Sci., 563 (2015), 99–143 | DOI | MR | Zbl

[13] M. Bernardo, “ULTraS at work: compositionality metaresults for bisimulation and trace semantics”, J. Log. Algebr. Methods Program., 94 (2018), 150–182 | DOI | MR | Zbl

[14] M. Bernardo, S. Botta, “Modal logic characterization of Markovian testing and trace equivalences”, Proceedings of the workshop on logic, models and computer science, LMCS 2006 (Camerino, Italy, April 20-22, 2006), Electronic Notes in Theoretical Computer Science, 169, eds. Corradini Flavio et al., Elsevier, Amsterdam, 2007, 7–18 | DOI | MR | Zbl

[15] M. Bernardo, S. Botta, “A survey of modal logics characterizing behavioural equivalences for non-deterministic and stochastic systems”, Math. Struct. Comput. Sci., 18:1 (2008), 29–55 | DOI | MR | Zbl

[16] M. Bernardo, M. Bravetti, Reward based congruences: Can we aggregate more?, Process algebra and probabilistic methods. Performance modelling and verification, Joint international workshop, PAPM-PROBMIV 2001 (Aachen, Germany, September 12-14, 2001), Lect. Notes Comput. Sci., 2165, eds. De Alfaro Luca et al., Springer, Berlin, 2001, 136–151 | DOI | MR | Zbl

[17] M. Bernardo, L. Donatiello, R. Gorrieri, “A formal approach to the integration of performance aspects in the modeling and analysis of concurrent systems”, Inf. Comput., 144:2 (1998), 83–154 | DOI | MR | Zbl

[18] M. Bernardo, R. Gorrieri, “A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time”, Theor. Comput. Sci., 202:1-2 (1998), 1–54 | DOI | MR | Zbl

[19] M. Bernardo, R. De Nicola, M. Loreti, “A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences”, Inf. Comput., 225 (2013), 29–82 | DOI | MR | Zbl

[20] M. Bernardo, L. Tesei, “Encoding timed models as uniform labeled transition systems”, Lect. Notes Comput. Sci., 8168, 2013, 104–118 | DOI

[21] E. Best, R. Devillers, J.G. Hall, “The box calculus: a new causal algebra with multi-label communication”, Lect. Notes Comput. Sci., 609, Springer, Berlin, 1992, 21–69 | DOI | MR

[22] E. Best, R. Devillers, M. Koutny, Petri net algebra, EATCS Monographs on Theoretical Computer Science, Springer, Berlin, 2000 | MR | Zbl

[23] E. Best, M. Koutny, “A refined view of the box algebra”, Application and theory of Petri nets 1995, 16th international conference, Proceedings (Turin, Italy, June 26-30, 1995), Lect. Notes in Comput. Sci., 935, eds. De Michelis Giorgio et al., 1995, 1–20 | DOI | MR | Zbl

[24] T. Bolognesi, F. Lucidi, S. Trigila, “From timed Petri nets to timed LOTOS”, Proc. IFIP WG 6.1 $10^{th}$ Int. Symposium on Protocol Specification, Testing and Verification (1990, Ottawa, Canada), North-Holland, Amsterdam, 1990, 1–14

[25] N. Bonzanni, K.A. Feenstra, W. Fokkink, E. Krepska, What can formal methods bring to systems biology?, Lect. Notes in Comput. Sci., 5850, 2009, 16–22 | DOI

[26] A.A. Borovkov, Probability theory, Springer, London, 2013 | MR | Zbl

[27] M. Bravetti, Specification and analysis of stochastic real-time systems, Ph. D. thesis, University of Bologna, Italy, 2002

[28] M. Bravetti, M. Bernardo, R. Gorrieri, “Towards performance evaluation with general distributions in process algebras”, Lect. Notes in Comput. Sci., 1466, Springer, Berlin–Heidelberg, 1998, 405–422 | DOI | MR

[29] P. Buchholz, “Markovian process algebra: composition and equivalence”, Proc. $2^{nd}$ Int. Workshop on Process Algebras and Performance Modelling (PAPM) 1994 (Regensberg / Erlangen, Germany, July 1994), Arbeitsberichte des IMMD, 27, no. 4, eds. U. Herzog, M. Rettelbach, 1994, 11–30

[30] P. Buchholz, “Exact and ordinary lumpability in finite Markov chains”, J. Appl. Probab., 31:1 (1994), 59–75 | DOI | MR | Zbl

[31] P. Buchholz, “A notion of equivalence for stochastic Petri nets”, Lect. Notes in Comput. Sci., 935, Springer, Berlin, 1995, 161–180 | DOI | MR | Zbl

[32] P. Buchholz, “Iterative decomposition and aggregation of labeled GSPNs”, Lect. Notes in Comput. Sci., 1420, Springer, Berlin, 1998, 226–245 | DOI | Zbl

[33] P. Buchholz, I.V. Tarasyuk, “Net and algebraic approaches to probabilistic modeling”, Jt. Bull. NCC IIS, Ser. Comput. Sci., 15 (2001), 31–64 | Zbl

[34] P. Buchholz, I.V. Tarasyuk, “Equivalences for stochastic Petri nets and stochastic process algebras”, Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform., 6:1 (2006), 14–42 | MR | Zbl

[35] I. Christoff, “Testing equivalence and fully abstract models of probabilistic processes”, Lect. Notes in Comput. Sci., 458, Springer, Berlin, 1990, 126–140 | DOI | MR

[36] N. Coste, H. Hermanns, E. Lantreibecq, W. Serwe, “Towards performance prediction of compositional models in industrial GALS designs”, Lect. Notes in Comput. Sci., 5643, Springer, Berlin, 2009, 204–218 | DOI | Zbl

[37] V. Danos, J. Feret, W. Fontana, R. Harmer, J. Krivine, “Rule-based modelling of cellular signalling”, Lect. Notes in Comput. Sci., 4703, Springer, Berlin, 2007, 17–41 | DOI | MR | Zbl

[38] S. Derisavi, H. Hermanns, W.H. Sanders, “Optimal state-space lumping of Markov chains”, Inf. Process. Lett., 87:6 (2003), 309–315 | DOI | MR | Zbl

[39] Ch. Eisentraut, H. Hermanns, J. Schuster, A. Turrini, L. Zhang, “The quest for minimal quotients for probabilistic automata”, Lect. Notes in Comput. Sci., 7795, Springer, Berlin, 2013, 16–31 | DOI | Zbl

[40] D. Gilbert, M. Heiner, S. Lehrack, “A unifying framework for modelling and analysing biochemical pathways using Petri nets”, Lect. Notes in Comput. Sci., 4695, Springer, Berlin–Heidelberg, 2007, 200–216 | DOI

[41] R.J. van Glabbeek, S.A. Smolka, B. Steffen, “Reactive, generative, and stratified models of probabilistic processes”, Inf. Comput., 121:1 (1995), 59–80 | DOI | MR | Zbl

[42] M.C. Guenther, N.J. Dingle, J.T. Bradley, W.J. Knottenbelt, “Passage-time computation and aggregation strategies for large semi-Markov processes”, Performance Evaluation, 68 (2011), 221–236 | DOI

[43] H.M. Hanish, “Analysis of place/transition nets with timed arcs and its application to batch process control”, Lect. Notes in Comput. Sci., 691, Springer, Berlin–Heidelberg, 1993, 282–299 | DOI | MR

[44] H. Hermanns, Interactive Markov chains. And the quest for quantified quality, Lect. Notes in Comput. Sci., 2428, Springer, Berlin, 2002 | MR | Zbl

[45] H. Hermanns, M. Rettelbach, “Syntax, semantics, equivalences and axioms for MTIPP $y$”, Proc. $2^{nd}$ Int. Workshop on Process Algebras and Performance Modelling (PAPM) 1994 (Regensberg / Erlangen, Germany, July 1994), Arbeitsberichte des IMMD, 27, no. 4, eds. U. Herzog, M. Rettelbach, 1994, 71–88

[46] J. Hillston, A compositional approach to performance modelling, Dissertation, University of Edinburgh, Edinburgh, 1994 ; Distinguished Dissertations in Computer Science, Cambridge University Press, Cambridge, UK, 2005 | MR | Zbl

[47] C.A.R. Hoare, Communicating sequential processes, Prentice-Hall, Englewood Cliffs, New Jersey etc, 1985 | MR | Zbl

[48] A. Horváth, M., Paolieri, L. Ridi, E. Vicario, “Probabilistic model checking of non-Markovian models with concurrent generally distributed timers”, 2011 Eighth International Conference on Quantitative Evaluation of SysTems (Aachen, Germany, 2011), 131–140

[49] A. Horváth, M., Paolieri, L. Ridi, E. Vicario, “Transient analysis of non-Markovian models using stochastic state classes”, Performance Evaluation, 69:7–8 (2012), 315–335 | DOI

[50] C.-C. Jou, S.A. Smolka, “Equivalences, congruences and complete axiomatizations for probabilistic processes”, Lect. Notes in Comput. Sci, 458, Springer, Berlin, 1990, 367–383 | DOI | MR

[51] M. Koutny, “A compositional model of time Petri nets”, Lect. Notes in Comput. Sci., 1825, Springer, Berlin, 2000, 303–322 | DOI | MR | Zbl

[52] V.G. Kulkarni, Modeling and analysis of stochastic systems, Texts in Statistical Science, 84, CRC Press, Boca Raton, 2010 | MR | Zbl

[53] L. Lakatos, L. Szeidl, M. Telek, Introduction to queueing systems with telecommunication applications, Springer, Cham, 2019 | MR | Zbl

[54] K.G. Larsen, A. Skou, “Bisimulation through probabilistic testing”, Inf. Comput., 94:1 (1991), 1–28 | DOI | MR | Zbl

[55] D. Latella, M. Massink, E.P. de Vink, “Bisimulation of labelled state-to-function transition systems coalgebraically”, Log. Methods Comput. Sci., 11:4 (2015), 16 | MR | Zbl

[56] H. Macià, V. Valero, D.C. Cazorla, F. Cuartero, “Introducing the iteration in sPBC”, Lect. Notes in Comput. Sci., 3235, Springer, Berlin, 2004, 292–308 | DOI | Zbl

[57] H. Macià, V. Valero, F. Cuartero, D. de Frutos, “A congruence relation for sPBC”, Form. Methods Syst. Des., 32:2 (2008), 85–128 | DOI | MR | Zbl

[58] H. Macià, V. Valero, F. Cuartero, M.C. Ruiz, “sPBC: a Markovian extension of Petri box calculus with immediate multiactions”, Fundam. Inform., 87:3–4 (2008), 367–406 | MR | Zbl

[59] H. Macià, V. Valero, F. Cuartero, M.C. Ruiz, I.V. Tarasyuk, “Modelling a video conference system with sPBC”, Appl. Math. Inf. Sci., 10:2 (2016), 475–493 | DOI | MR

[60] H. Macià, V. Valero, D. de Frutos, “sPBC: a Markovian extension of finite Petri box calculus”, Proc. $9^{th}$ IEEE Int. Workshop on Petri Nets and Performance Models (PNPM) (Aachen, Germany, 2001), 207–216

[61] A. Marin, C. Piazza, S. Rossi, “Proportional lumpability”, Lect. Notes in Comput. Sci., 11750, Springer, Cham, 2019, 265–281 | DOI | Zbl

[62] A. Marin, C. Piazza, S. Rossi, “Proportional lumpability and proportional bisimilarity”, Acta Inf., 59:2-3 (2022) | DOI | MR | Zbl

[63] O. Marroquín, D. de Frutos, TPBC: timed Petri box calculus, Technical Report, Departamento de Sistemas Infofmáticos y Programación, Universidad Complutense de Madrid, Spain, 2000

[64] O. Marroquín, D. de Frutos, “Extending the Petri box calculus with time”, Lect. Notes in Comput. Sci., 2075, Springer, Berlin, 2001, 303–322 | DOI | MR | Zbl

[65] M.A. Marsan, “Stochastic Petri nets: an elementary introduction”, Lect. Notes in Comput. Sci., 424, Springer, Berlin–Heidelberg, 1990, 1–29 | DOI | MR

[66] M.A. Marsan, G. Balbo, G. Conte, S. Donatelli, G. Franceschinis, Modelling with generalised stochastic Petri nets, Wiley Series in Parallel Computing, John Wiley and Sons, Chichester, 1995 | Zbl

[67] Ph.M. Merlin, D.J. Farber, “Recoverability of communication protocols – implications of a theoretical study”, IEEE Trans. Commun., 24:9 (1976), 1036–1043 | DOI | MR | Zbl

[68] R.A.J. Milner, Communication and concurrency, Prentice-Hall, New York etc., 1989 | Zbl

[69] M.K. Molloy, On the integration of the throughput and delay measures in distributed processing models, Ph.D. thesis, Report, CSD-810-921, University of California, Los Angeles, 1981

[70] M.K. Molloy, “Discrete time stochastic Petri nets”, IEEE Trans. Software Eng., 11:4 (1985), 417–423 | DOI | MR | Zbl

[71] A. Niaouris, “An algebra of Petri nets with arc-based time restrictions”, Lect. Notes in Comput. Sci., 3407, Springer, Berlin, 2005, 447–462 | DOI | MR | Zbl

[72] A. Niaouris, M. Koutny, An algebra of timed-arc Petri nets, Technical Report, CS-TR-895, School of Computer Science, University of Newcastle upon Tyne, UK, 2005

[73] R. Paige, R.E. Tarjan, “Three partition refinement algorithms”, SIAM J. Comput., 16:6 (1987), 973–989 | DOI | MR | Zbl

[74] C. Priami, “Language-based performance prediction for distributed and mobile systems”, Inf. Computat., 175:2 (2002), 119–145 | DOI | MR | Zbl

[75] C. Ramchandani, Performance evaluation of asynchronous concurrent systems by timed Petri nets, Ph.D. thesis, Department of Electrical Engineering, Massachusetts Institute of Technology, Cambridge, Massachusetts, USA, 1973

[76] S.M. Ross, Stochastic processes, John Wiley and Sons, New York, 1996 | MR | Zbl

[77] S.M. Ross, Introduction to probability models, Elsevier/Academic Press, Amsterdam, 2019 | MR | Zbl

[78] A.N. Shiryaev, Probability-2, Graduate Texts in Mathematics, 95, Springer, New York, 2019 | DOI | MR | Zbl

[79] W.J. Stewart, Probability, Markov chains, queues, and simulation. The mathematical basis of performance modeling, Princeton University Press, Princeton, 2009 | MR | Zbl

[80] I.V. Tarasyuk, Discrete time stochastic Petri box calculus, Berichte aus dem Department für Informatik, No 3/05, Carl von Ossietzky Universität Oldenburg, Germany, 2005

[81] I.V. Tarasyuk, “Iteration in discrete time stochastic Petri box calculus”, Jt. Bull. NCC IIS, Ser. Comput. Sci., 24 (2006), 129–148 | MR | Zbl

[82] I.V. Tarasyuk, “Stochastic Petri box calculus with discrete time”, Fundam. Inform., 76:1-2 (2007), 189–218 | MR | Zbl

[83] I.V. Tarasyuk, Equivalences for behavioural analysis of concurrent and distributed computing systems, Geo Academic Publisher, Novosibirsk, Russia, 2007

[84] I.V. Tarasyuk, “Equivalence relations for modular performance evaluation in dtsPBC”, Math. Struct. Comput. Sci., 24:1 (2014), e240103 | DOI | MR | Zbl

[85] I.V. Tarasyuk, “Discrete time stochastic and deterministic Petri box calculus dtsdPBC”, Sib. Èlektron. Mat. Izv., 17 (2020), 1598–1679 | DOI | MR | Zbl

[86] I.V. Tarasyuk, “Performance evaluation in stochastic process algebra dtsdPBC”, Sib. Èlektron. Mat. Izv., 18:2 (2021), 1105–1145 | DOI | MR | Zbl

[87] I.V. Tarasyuk, Stochastic bisimulation and performance evaluation in discrete time stochastic and deterministic Petri box calculus dtsdPBC, , HAL Open Archives, France, 2023 hal-02573419v4

[88] I.V. Tarasyuk, H. Macià, V. Valero, Discrete time stochastic Petri box calculus with immediate multiactions, Technical Report, No DIAB-10-03-1, Department of Computer Systems, High School of Computer Science Engineering, University of Castilla - La Mancha, Albacete, Spain, 2010

[89] I.V. Tarasyuk, H. Macià, V. Valero, “Discrete time stochastic Petri box calculus with immediate multiactions dtsiPBC”, Electronic Notes in Theoretical Computer Science, 296 (2013), 229–252 | DOI

[90] I.V. Tarasyuk, H. Macià, V. Valero, “Performance analysis of concurrent systems in algebra dtsiPBC”, Program. Comput. Softw., 40:5 (2014), 229–249 | DOI | MR | Zbl

[91] I.V. Tarasyuk, H. Macià, V. Valero, “Stochastic process reduction for performance evaluation in dtsiPBC”, Sib. Èlektron. Mat. Izv., 12 (2015), 513–551 | MR | Zbl

[92] I.V. Tarasyuk, H. Macià, V. Valero, “Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC”, Sib. Èlektron. Mat. Izv., 15 (2018), 1743–1812 | DOI | MR | Zbl

[93] M. Timmer, J.-P. Katoen, J. van de Pol, M.I.A. Stoelinga, “Efficient modelling and generation of Markov automata”, Lect. Notes in Comput. Sci., 7454, Springer, Berlin, 2012, 364–379 | DOI | MR | Zbl

[94] K.S. Trivedi, Probability and statistics with reliability, queuing, and computer science applications, John Wiley Sons, Hobokenn, 2016 | MR | Zbl

[95] V. Valero, M.E. Cambronero, “Using unified modelling language to model the publish/subscribe paradigm in the context of timed Web services with distributed resources”, Mathematical and Computer Modelling of Dynamical Systems, 23:6 (2017), 570–594 | DOI

[96] R. Wimmer, S. Derisavi, H. Hermanns, “Symbolic partition refinement with automatic balancing of time and space”, Performance Evaluation, 67:9 (2010), 816–836 | DOI

[97] R. Zijal, “Discrete time deterministic and stochastic Petri nets”, Proc. Int. Workshop on Quality of Communication-Based Systems (1994, Technical University of Berlin, Germany), Kluwer Academic Publishers, Dordrecht, 1995, 123–136 | DOI | Zbl

[98] R. Zijal, Analysis of discrete time deterministic and stochastic Petri nets, Ph.D. thesis, Technical University of Berlin, Germany, 1997

[99] R. Zijal, R. German, “A new approach to discrete time stochastic Petri nets”, $11^{th} $ Int. Conf. on Analysis and Optimization of Systems, Discrete Event Systems, Lecture Notes in Control and Information Sciences, 199, eds. Cohen G., Quadrat JP., Springer, Berlin–Heidelberg, 1994, 198–204 | DOI | MR