Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC

I. V. Tarasyuk ; H. Macià ; V. Valero

Sibirskie èlektronnye matematičeskie izvestiâ, Tome 15 (2018), pp. 1743-1812.

Résumé

We propose an extension with immediate multiactions of discrete time stochastic Petri Box Calculus (dtsPBC), presented by I.V. Tarasyuk. The resulting algebra dtsiPBC is a discrete time analogue of stochastic Petri Box Calculus (sPBC) with immediate multiactions, designed by H. Macìa, V. Valero et al. within a continuous time domain. The step operational semantics is constructed via labeled probabilistic transition systems. The denotational semantics is based on labeled discrete time stochastic Petri nets with immediate transitions. To evaluate performance, the corresponding semi-Markov chains are analyzed. We define step stochastic bisimulation equivalence of expressions that is applied to reduce their transition systems and underlying semi-Markov chains while preserving the functionality and performance characteristics. We explain how this equivalence can be used to simplify performance analysis of the algebraic processes. In a case study, a method of modeling, performance evaluation and behaviour reduction for concurrent systems is outlined and applied to the shared memory system.

Détail

Keywords: stochastic process algebra, Petri box calculus, discrete time, immediate multiaction, operational and denotational semantics, performance evaluation, stochastic equivalence, reduction.
Mots-clés : semi-Markov chain

Bibliographie

[1] W.M.P. van der Aalst, K.M. van Hee, H.A. Reijers, “Analysis of discrete-time stochastic Petri nets”, Statistica Neerlandica, 54:2 (2000), 237–255 https://www.win.tue.nl/h̃reijers/H.A. | DOI | MR | Zbl

[2] C. Autant, Ph. Schnoebelen, “Place bisimulations in Petri nets”, Lecture Notes in Computer Science, 616, 1992, 45–61 | DOI | MR

[3] C. Baier, “Polynomial time algorithms for testing probabilistic bisimulation and simulation”, Lecture Notes in Computer Science, 1102, 1996, 50–61 | DOI

[4] C. Baier, B. Engelen, M. Majster-Cederbaum, “Deciding bisimilarity and similarity for probabilistic processes”, Journal of Computer and System Sciences, 60:1 (2000), 187–231 | DOI | MR | Zbl

[5] G. Balbo, “Introduction to stochastic Petri nets”, Lecture Notes in Computer Science, 2090, 2001, 84–155 | DOI | Zbl

[6] G. Balbo, “Introduction to generalized stochastic Petri nets”, Lecture Notes in Computer Science, 4486, 2007, 83–131 | DOI | Zbl

[7] F. Bause, P.S. Kritzinger, Stochastic Petri nets: an introduction to the theory, Vieweg Verlag, Wiesbaden, 2002 http://ls4-www.cs.tu-dortmund.de/cms/de/home/bause/bause_kritzinger_spn_book_print.pdf | Zbl

[8] J.A. Bergstra, J.W. Klop, “Algebra of communicating processes with abstraction”, Theoretical Computer Science, 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, 276 pp. http://www.sti.uniurb.it/bernardo/documents/phdthesis.pdf

[10] M. Bernardo, “A survey of Markovian behavioral equivalences”, Lecture Notes in Computer Science, 4486, 2007, 180–219 | DOI | Zbl

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

[12] M. Bernardo, M. Bravetti, Reward based congruences: can we aggregate more?, Lecture Notes in Computer Science, 2165, 2001, 136–151 http://www.sti.uniurb.it/bernardo/documents/papmprobmiv2001.pdf | DOI | MR | Zbl

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

[14] M. Bernardo, R. Gorrieri, “A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time”, Theoretical Computer Science, 202:1–2 (1998), 1–54 | DOI | MR | Zbl

[15] E. Best, R. Devillers, J.G. Hall, “The box calculus: a new causal algebra with multi-label communication”, Lecture Notes in Computer Science, 609, 1992, 21–69 | DOI | MR

[16] E. Best, R. Devillers, M. Koutny, Petri net algebra, EATCS Monographs on Theoretical Computer Science, Springer, Berlin, 2001 | DOI | MR

[17] E. Best, M. Koutny, “A refined view of the box algebra”, Lecture Notes in Computer Science, 935, 1995, 1–20 | DOI | MR

[18] J.T. Bradley, “Semi-Markov PEPA: modelling with generally distributed actions”, International Journal of Simulation, 6:3–4 (2005), 43–51 http://pubs.doc.ic.ac.uk/semi-markov-pepa/semi-markov-pepa.pdf

[19] M. Bravetti, Specification and analysis of stochastic real-time systems, Ph.D. thesis, University of Bologna, Italy, 2002, 432 pp. http://www.cs.unibo.it/b̃ravetti/papers/phdthesis.ps.gz

[20] M. Bravetti, P.R. D'Argenio, “Tutte le algebre insieme: concepts, discussions and relations of stochastic process algebras with general distributions”, Lecture Notes in Computer Science, 2925, 2004, 44–88 | DOI | Zbl

[21] M. Bravetti, M. Bernardo, R. Gorrieri, “Towards performance evaluation with general distributions in process algebras”, Lecture Notes in Computer Science, 1466, 1998, 405–422 | DOI | MR

[22] E. Brinksma, H. Hermanns, “Process algebra and Markov chains”, Lecture Notes in Computer Science, 2090, 2001, 183–231 | DOI | MR | Zbl

[23] E. Brinksma, J.-P. Katoen, R. Langerak, D. Latella, “A stochastic causality-based process algebra”, The Computer Journal, 38:7 (1995), 552–565 | DOI

[24] G. Bucci, L. Sassoli, E. Vicario, “Correctness verification and performance analysis of real-time systems using stochastic preemptive time Petri nets”, IEEE Transactions on Software Engineering, 31:11 (2005), 913–927 | DOI

[25] 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

[26] P. Buchholz, “Exact and ordinary lumpability in finite Markov chains”, Journal of Applied Probability, 31:1 (1994), 59–75 | DOI | MR | Zbl

[27] P. Buchholz, “A notion of equivalence for stochastic Petri nets”, Lecture Notes in Computer Science, 935, 1995, 161–180 | DOI | MR

[28] P. Buchholz, “Iterative decomposition and aggregation of labeled GSPNs”, Lecture Notes in Computer Science, 1420, 1998, 226–245 | DOI

[29] P. Buchholz, I.V. Tarasyuk, “Net and algebraic approaches to probabilistic modeling”, Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science, 15 (2001), 31–64 | Zbl

[30] S. Cattani, R. Segala, “Decision algorithms for probabilistic bisimulation”, Lecture Notes in Computer Science, 2421, 2002, 371–385 | DOI | MR | Zbl

[31] I. Christoff, “Testing equivalence and fully abstract models of probabilistic processes”, Lecture Notes in Computer Science, 458, 1990, 126–140 | DOI | MR

[32] C. Daws, “Symbolic and parametric model checking of discrete-time Markov chains”, Lecture Notes in Computer Science, 3407, 2005, 280–294 | DOI | MR | Zbl

[33] P. Degano, C. Priami, “Non-interleaving semantics for mobile processes”, Theoretical Computer Science, 216:1–2 (1999), 237–270 | DOI | MR | Zbl

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

[35] Ch. Eisentraut, H. Hermanns, J. Schuster, A. Turrini, L. Zhang, “The quest for minimal quotients for probabilistic automata”, Lecture Notes in Computer Science, 7795, 2013, 16–31 | DOI | MR | Zbl

[36] J.M. Fourneau, “Collaboration of discrete-time Markov chains: tensor and product form”, Performance Evaluation, 67 (2010), 779–796 | DOI

[37] S. Gilmore, J. Hillston, L. Kloul, M. Ribaudo, “PEPA nets: a structured performance modelling formalism”, Performance Evaluation, 54 (2003), 79–104 | DOI

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

[39] N. Götz, U. Herzog, M. Rettelbach, “Multiprocessor and distributed system design: the integration of functional specification and performance analysis using stochastic process algebras”, Lecture Notes in Computer Science, 729, 1993, 121–146 | DOI

[40] 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

[41] T. Han, J.-P. Katoen, A. Mereacre, “Approximate parameter synthesis for probabilistic time-bounded reachability”, Proc. $29^{th}$ IEEE Real-Time Systems Symposium (RTSS) 2008 (New York, USA), IEEE Computer Society Press, 2008, 173–182 | DOI

[42] B.R. Haverkort, “Markovian models for performance and dependability evaluation”, Lecture Notes in Computer Science, 2090, 2001, 38–83 | DOI | Zbl

[43] R.A. Hayden, J.T. Bradley, A. Clark, “Performance specification and evaluation with unified stochastic probes and fluid analysis”, IEEE Transactions on Software Engineering, 39:1 (2013), 97–118 | DOI

[44] H. Hermanns, M. Rettelbach, “Syntax, semantics, equivalences and axioms for MTIPP”, 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 http://ftp.informatik.uni-erlangen.de/local/inf7/papers/Hermanns/syntax_semantics_equivalences_axioms_for_MTIPP.ps.gz

[45] J. Hillston, “The nature of synchronisation”, Proc. $2^{nd}$ Int. Workshop on Process Algebra and Performance Modelling (PAPM) 1994 (Regensberg, Erlangen, Germany, July 1994), Arbeitsberichte des IMMD, 27, no. 4, eds. U. Herzog, M. Rettelbach, 1994, 51–70 http://www.dcs.ed.ac.uk/pepa/synchronisation.pdf

[46] J. Hillston, A compositional approach to performance modelling, Cambridge University Press, Cambridge, 1996 http://www.dcs.ed.ac.uk/pepa/book.pdf | MR

[47] C.A.R. Hoare, Communicating sequential processes, Prentice-Hall, London, UK, 1985 http://www.usingcsp.com/cspbook.pdf | MR | Zbl

[48] 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

[49] L. Jategaonkar, A.R. Meyer, “Deciding true concurrency equivalences on safe, finite nets”, Theoretical Computer Science, 154:1 (1996), 107–143 | DOI | MR | Zbl

[50] C.-C. Jou, S.A. Smolka, “Equivalences, congruences and complete axiomatizations for probabilistic processes”, Lecture Notes in Computer Science, 458, 1990, 367–383 | DOI | MR

[51] G. Kahn, “Natural semantics”, Proc. $4^{th}$ Annual Symposium on Theoretical Aspects of Computer Science (STACS) 1987, Springer, 1987, 22–39 | MR

[52] J.-P. Katoen, Quantitative and qualitative extensions of event structures, Ph.D. thesis, CTIT Ph.D.-thesis series, 96-09, Centre for Telematics and Information Technology, University of Twente, Enschede, The Netherlands, 1996

[53] J.-P. Katoen, P.R. D'Argenio, “General distributions in process algebra”, Lecture Notes in Computer Science, 2090, 2001, 375–429 | DOI | Zbl

[54] J.-P. Katoen, E. Brinksma, D. Latella, R. Langerak, “Stochastic simulation of event structures”, Proc. $4^{th}$ Int. Workshop on Process Algebra and Performance Modelling (PAPM) 1996, ed. M. Ribaudo, CLUT Press, Torino, Italy, 1996, 21–40 http://eprints.eemcs.utwente.nl/6487/01/263_KLLB96b.pdf

[55] V.G. Kulkarni, Modeling and analysis of stochastic systems, Texts in Statistical Science, 84, Second edition, Chapman and Hall / CRC Press, 2009 | MR

[56] R. Lanotte, A. Maggiolo-Schettini, A. Troina, “Parametric probabilistic transition systems for system design and analysis”, Formal Aspects of Computing, 19:1 (2007), 93–109 | DOI | Zbl

[57] K.G. Larsen, A. Skou, “Bisimulation through probabilistic testing”, Information and Computation, 94:1 (1991), 1–28 | DOI | MR | Zbl

[58] H. Macià, V. Valero, D.C. Cazorla, F. Cuartero, “Introducing the iteration in sPBC”, Lecture Notes in Computer Science, 3235, 2004, 292–308 | DOI | Zbl

[59] H. Macià, V. Valero, F. Cuartero, D. de Frutos, “A congruence relation for sPBC”, Formal Methods in System Design, 32:2 (2008), 85–128 | DOI | MR | Zbl

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

[61] 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) 2001 (Aachen, Germany), IEEE Computer Society Press, 2001, 207–216 http://www.info-ab.uclm.es/retics/publications/2001/pnpm01.ps

[62] J. Markovski, P.R. D'Argenio, J.C.M. Baeten, E.P. de Vink, “Reconciling real and stochastic time: the need for probabilistic refinement”, Formal Aspects of Computing, 24:4–6 (2012), 497–518 | DOI | MR | Zbl

[63] J. Markovski, E.P. de Vink, “Extending timed process algebra with discrete stochastic time”, Lecture Notes of Computer Science, 5140, 2008, 268–283 | DOI | Zbl

[64] J. Markovski, E.P. de Vink, “Performance evaluation of distributed systems based on a discrete real- and stochastic-time process algebra”, Fundamenta Informaticae, 95:1 (2009), 157–186 | MR | Zbl

[65] M.A. Marsan, “Stochastic Petri nets: an elementary introduction”, Lecture Notes in Computer Science, 424, 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, 1995 http://www.di.unito.it/g̃reatspn/GSPN-Wiley/ | Zbl

[67] R.A.J. Milner, Communication and concurrency, Prentice-Hall, Upper Saddle River, NJ, USA, 1989 | Zbl

[68] R.A.J. Milner, J.G. Parrow, D.J. Walker, “A calculus of mobile processes (I and II)”, Information and Computation, 100:1 (1992), 1–77 | DOI | MR | Zbl

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

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

[71] U. Montanari, M. Pistore, D. Yankelevich, “Efficient minimization up to location equivalence”, Lecture Notes in Computer Science, 1058, 1996, 265–279 | DOI

[72] T.N. Mudge, H.B. Al-Sadoun, “A semi-Markov model for the performance of multiple-bus systems”, IEEE Transactions on Computers, C-34:10 (1985), 934–942 | DOI

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

[74] G.D. Plotkin, A structural approach to operational semantics, Technical Report, No DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981

[75] C. Priami, “Stochastic $\pi$-calculus with general distributions”, Proc. $4^{th}$ Int. Workshop on Process Algebra and Performance Modelling (PAPM) 1996, ed. M. Ribaudo, CLUT Press, Torino, Italy, 1996, 41–57

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

[77] M. Rettelbach, “Probabilistic branching in Markovian process algebras”, The Computer Journal, 38:7 (1995), 590–599 | DOI

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

[79] I.V. Tarasyuk, Discrete time stochastic Petri box calculus, Berichte aus dem Department für Informatik, 3/05, Carl von Ossietzky Universität Oldenburg, Germany, 2005 http://itar.iis.nsk.su/files/itar/pages/dtspbcib_cov.pdf

[80] I.V. Tarasyuk, “Iteration in discrete time stochastic Petri box calculus”, Bulletin of the Novosibirsk Computing Center, Series Computer Science, 24, IIS Special Issue (2006), 129–148 | Zbl

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

[82] I.V. Tarasyuk, “Equivalence relations for modular performance evaluation in dtsPBC”, Mathematical Structures in Computer Science, 24:1 (2014), e240103 | MR | Zbl

[83] I.V. Tarasyuk, H. Macià, V. Valero, “Discrete time stochastic Petri box calculus with immediate multiactions dtsiPBC” (London, UK, 2012), Electronic Notes in Theoretical Computer Science, 296, Proc. $6^{th}$ Int. Workshop on Practical Applications of Stochastic Modelling (PASM) 2012 and $11^{th}$ Int. Workshop on Parallel and Distributed Methods in Verification (PDMC) 2012 (2013), 229–252 | DOI

[84] I.V. Tarasyuk, H. Macià, V. Valero, “Performance analysis of concurrent systems in algebra dtsiPBC”, Programming and Computer Software, 40:5 (2014), 229–249 | DOI | MR | Zbl

[85] I.V. Tarasyuk, H. Macià, V. Valero, “Stochastic process reduction for performance evaluation in dtsiPBC”, Siberian Electronic Mathematical Reports, 12 (2015), 513–551 | MR | Zbl

[86] 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

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

[88] R. Zijal, G. Ciardo, G. Hommel, “Discrete deterministic and stochastic Petri nets”, Proc. $9^{th}$ ITG/GI Professional Meeting on Measuring, Modeling and Evaluation of Computer and Communication Systems (MMB) 1997 (Freiberg, Germany, 1997), v. 1, eds. K. Irmscher, Ch. Mittasch, K. Richter, VDE-Verlag, Berlin, Germany, 1997, 103–117 http://www.cs.ucr.edu/c̃iardo/pubs/1997MMB-DDSPN.pdf

[89] A. Zimmermann, J. Freiheit, G. Hommel, “Discrete time stochastic Petri nets for modeling and evaluation of real-time systems”, Proc. $9^{th}$ Int. Workshop on Parallel and Distributed Real Time Systems (WPDRTS) 2001 (San Francisco, USA), 2001, 282–286 http://pdv.cs.tu-berlin.de/ãzi/texte/WPDRTS01.pdf