Geodesic
Discrete time stochastic and deterministic Petri box calculus dtsdPBC
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 1598-1679.

Voir la notice de l'article provenant de la source Math-Net.Ru

We propose dtsdPBC, an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Macià and V. Valero. dtsdPBC enhances the expressiveness of dtsiPBC and extends the application area of the associated specification and analysis techniques. In dtsdPBC, non-negative integers are used to specify fixed (including zero) time delays of deterministic multiactions. The step operational semantics of the calculus is constructed via labeled probabilistic transition systems. The Petri net denotational semantics of the calculus is defined on the basis of dtsd-boxes, a subclass of novel labeled discrete time stochastic Petri nets with deterministic transitions (LDTSDPNs). We also define step stochastic bisimulation equivalence of the algebraic expressions, used to compare the qualitative and quantitative behaviour of the specified processes. The consistency of the operational and denotational semantics of dtsdPBC up to that bisimulation equivalence is established. The interrelations of the mentioned equivalence with other behavioural notions of the calculus are investigated. A series of examples that construct the transition systems and dtsd-boxes for the expressions with different types of multiactions and operations demonstrates both the specification capabilities and semantic features of the new calculus.
Keywords: stochastic process algebra, stochastic Petri net, Petri box calculus, discrete time, deterministic multiaction, transition system, operational semantics, stochastic transition, deterministic transition, dtsd-box, denotational semantics, stochastic bisimulation.
Mots-clés : stochastic multiaction 
@article{SEMR_2020_17_a36,
     author = {I. V. Tarasyuk},
     title = {Discrete time stochastic and deterministic {Petri} box calculus {dtsdPBC}},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {1598--1679},
     publisher = {mathdoc},
     volume = {17},
     year = {2020},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2020_17_a36/}
}
TY  - JOUR
AU  - I. V. Tarasyuk
TI  - Discrete time stochastic and deterministic Petri box calculus dtsdPBC
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2020
SP  - 1598
EP  - 1679
VL  - 17
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2020_17_a36/
LA  - en
ID  - SEMR_2020_17_a36
ER  - 
%0 Journal Article
%A I. V. Tarasyuk
%T Discrete time stochastic and deterministic Petri box calculus dtsdPBC
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2020
%P 1598-1679
%V 17
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2020_17_a36/
%G en
%F SEMR_2020_17_a36
I. V. Tarasyuk. Discrete time stochastic and deterministic Petri box calculus dtsdPBC. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 1598-1679. http://geodesic.mathdoc.fr/item/SEMR_2020_17_a36/

[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. Reijers Bestanden/Statistica.pdf | DOI | MR | Zbl

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

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

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

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

[6] J.A. Bergstra, J.W. Klop, “Algebra of communicating processes with abstraction”, Theoretical Computer Science, 37 (1985), 77–121 | DOI | MR | Zbl

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

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

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

[10] M. Bernardo, S. Botta, “Modal logic characterization of Markovian testing and trace equivalences”, Electronic Notes in Theoretical Computer Science, 169 (2006), 7–18 | DOI | MR | Zbl

[11] M. Bernardo, S. Botta, “A survey of modal logics characterizing behavioural equivalences for non-deterministic and stochastic systems”, Mathematical Structures in Computer Science, 18 (2008), 29–55 | DOI | MR | Zbl

[12] M. Bernardo, M. Bravetti, Reward based congruences: can we aggregate more?, Lecture Notes in Computer Science, 2165, 2001, 136–151 | 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 (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, 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] 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 (1990, Ottawa, Canada), North-Holland, Amsterdam, The Netherlands, 1–14 | MR

[19] N. Bonzanni, K.A. Feenstra, W. Fokkink, E. Krepska, What can formal methods bring to systems biology?, Lecture Notes in Computer Science, 5850, 2009, 16–22 | DOI

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

[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, “A notion of equivalence for stochastic Petri nets”, Lecture Notes in Computer Science, 935, 1995, 161–180 | DOI | MR

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

[28] 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 | MR | Zbl

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

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

[31] G. Ciardo, “Discrete-time Markovian stochastic Petri nets”, Computations with Markov Chains, NSMC 1995, Proc. $2^{nd}$ Int. Workshop on the Numerical Solution of Markov Chains (Raleigh, NC, USA, January 1995), ed. W.J. Stewart, Kluwer, Boston, MA, USA, 1995, 339–358 http://web.cs.iastate.edu/c̃iardo/pubs/1995NSMC-Discrete.pdf | DOI | Zbl

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

[33] H.M. Hanish, “Analysis of place/transition nets with timed-arcs and its application to batch process control”, Lecture Notes in Computer Science, 691, 1993, 282–299 | DOI | MR

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

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

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

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

[38] A. Horváth, A. Puliafito, M. Scarpa, M. Telek, “Analysis and evaluation of non-Markovian stochastic Petri nets”, Lecture Notes in Computer Science, 1786, 2000, 171–187 | DOI | Zbl

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

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

[41] M. Koutny, “A compositional model of time Petri nets”, Lecture Notes in Computer Science, 1825, 2000, 303–322 | DOI | MR | Zbl

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

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

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

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

[46] H. Macià, V. Valero, F. Cuartero, M.C. Ruiz, I.V. Tarasyuk, “Modelling a video conference system with sPBC”, Applied Mathematics and Information Sciences, 10:2 (2016), 475–493 | DOI | MR

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

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

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

[50] 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 | DOI | MR | Zbl

[51] 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, Madrid, Spain, 2000 (in Spanish)

[52] O. Marroquín, D. de Frutos, “Extending the Petri box calculus with time”, Lecture Notes in Computer Science, 2075, 2001, 303–322 | DOI | MR | Zbl

[53] M.A. Marsan, “Stochastic Petri nets: an elementary introduction”, Lecture Notes in Computer Science, 424, 1990, 1–29 | DOI | MR

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

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

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

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

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

[59] A. Niaouris, “An algebra of Petri nets with arc-based time restrictions”, Lecture Notes in Computer Science, 3407, 2005, 447–462 | DOI | MR | Zbl

[60] 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, 60 pp. http://www.cs.ncl.ac.uk/publications/trs/papers/895.pdf

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

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

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

[64] 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, 25 pp. http://itar.iis.nsk.su/files/itar/pages/dtspbcib_cov.pdf

[65] 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 | MR | Zbl

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

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

[68] 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, 25 pp. http://www.dsi.uclm.es/descargas/technicalreports/DIAB-10-03-1/dtsipbc.pdf

[69] I.V. Tarasyuk, H. Macià, V. Valero, “Discrete time stochastic Petri box calculus with immediate multiactions dtsiPBC”, 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 (London, UK, 2012), Electronic Notes in Theoretical Computer Science, 296, eds. J. Bradley, K. Heljanko, W. Knottenbelt, N. Thomas, 2013, 229–252 | DOI

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

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

[72] I.V. Tarasyuk, H. Macià, V. Valero, “Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC”, Siberian Electronic Mathematical Reports, 15 (2018), 1743–1812 | MR | Zbl

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

[74] 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, 1995, 123–136 | DOI | Zbl

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

[76] R. Zijal, G. Ciardo, Discrete deterministic and stochastic Petri nets, ICASE Report, No 96-72, Institute for Computer Applications in Science and Engineering (ICASE), NASA, Langley Research Centre, Hampton, VA, USA, 1996, 23 pp. ; http://www.dtic.mil/dtic/tr/fulltext/u2/a322409.pdfhttp://www.cs.odu.edu/m̃ln/ltrs-pdfs/icase-1996-72.pdf

[77] 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, 103–117, Berlin, Germany, 1997 http://www.cs.ucr.edu/c̃iardo/pubs/1997MMB-DDSPN.pdf

[78] R. Zijal, R. German, “A new approach to discrete time stochastic Petri nets”, Proc. $11^{th}$ Int. Conf. on Analysis and Optimization of Systems, Discrete Event Systems, DES 1994 (Sophia-Antipolis, France, 1994), Lecture Notes in Control and Information Sciences, 199, eds. G. Cohen, J.-P. Quadrat, 1994, 198–204 | DOI | MR

[79] A. Zimmermann, “Modeling and evaluation of stochastic Petri nets with TimeNET 4.1”, Proc. $6^{th}$ Int. ICST Conf. on Performance Evaluation Methodologies and Tools, VALUETOOLS 2012 (Cargèse, France, October 2012), eds. B. Gaujal, A. Jean-Marie, E. Jorswieck, A. Seuret, IEEE Computer Society Press, 2012, 1–10 https://www.tu-ilmenau.de/fileadmin/public/sse/Veroeffentlichungen/2012/VALUETOOLS2012.pdf

[80] A. Zimmermann, J. Freiheit, R. German, G. Hommel, “Petri net modelling and performability evaluation with TimeNET 3.0”, Lecture Notes in Computer Science, 1786, 2000, 188–202 | DOI | Zbl

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