Stochastic Petri Box Calculus with Discrete Time

• Autorzy: Tarasyuk I.V.
• Języki publikacji: EN

Abstrakty

EN

In the last decades, a number of stochastic enrichments of process algebras was constructed to allow one for specification of stochastic processes within the well-developed framework of algebraic calculi. In [], a continuous time stochastic extension of finite Petri box calculus (PBC) was proposed called sPBC. The algebra sPBC has interleaving semantics due to the properties of continuous time distributions. At the same time, PBC has step semantics, and it could be natural to propose its concurrent stochastic enrichment. We construct a discrete time stochastic extension dtsPBC of finite PBC. A step operational semantics is defined in terms of labeled transition systems based on action and inaction rules. A denotational semantics is defined in terms of a subclass of labeled discrete time stochastic Petri nets (LDTSPNs) called discrete time stochastic Petri boxes (dts-boxes). A consistency of both semantics is demonstrated. In addition, we define a variety of probabilistic equivalences that allow one to identify stochastic processes with similar behaviour which are differentiated by too strict notion of the semantic equivalence. The interrelations of all the introduced equivalences are investigated.

Słowa kluczowe

EN

stochastic Petri nets; stochastic process algebras; Petri box calculus; discrete time; transition systems; operational semantics; dts-boxes; denotational semantics; empty loops; probabilistic equivalences

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 76, nr 1-2
• Strony: 189--218
• Opis fizyczny: bibliogr. 49 poz., rys.

Twórcy

autor

Tarasyuk I.V.

• A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences, 6, Acad. Lavrentiev avenue, 630090, Novosibirsk, Russia,

Bibliografia

• [1] Andova, S.: Process algebra with probabilistic choice, Lecture Notes in Computer Science, 1601, 1999, 111-129.
• [2] Bernardo, M., Gorrieri, R.: A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time, Theoretical Computer Science, 202, July 1998, 1-54.
• [3] Best, E., Devillers, R., Esparza, J.: General refinement and recursion operations in the box calculus, Lecture Notes in Computer Science, 665, 1993, 130-140.
• [4] Best, E., Devillers, R., Hall, J. G.: The box calculus: a new causal algebra with multi-label communication, Lecture Notes in Computer Science, 609, 1992, 21-69.
• [5] Best, E., Devillers, R., Koutny, M.: Petri nets, process algebras and concurrent programming languages, Lecture Notes in Computer Science, 1492, 1998, 1-84, Http://parsys.informatik.unioldenburg.de/˜best/publications/apnf.ps.gz.
• [6] Best, E., Devillers, R., Koutny,M.: Petri net algebra, EATCSMonographs on Theoretical Computer Science, Springer Verlag, 2001, 378 pages.
• [7] Best, E., Devillers, R., Koutny, M.: The box algebra = Petri nets + process expressions, Information and Computation, 178, 2002, 44-100.
• [8] Best, E., Koutny, M.: A refined view of the box algebra, Lecture Notes in Computer Science, 935, 1995, 1-20.
• [9] Buchholz, P.: Markovian process algebra: composition and equivalence, Proceedings of 2nd Workshop on Process Algebras and Performance Modelling (U. Herzog, M. Rettelbach, Eds.), 27, University of Erlangen, Germany, 1994.
• [10] Buchholz, P.: A notion of equivalence for stochastic Petri nets, Lecture Notes in Computer Science, 935, 1995, 161-180.
• [11] Buchholz, P.: Iterative decomposition and aggregation of labeled GSPNs, Lecture Notes in Computer Science, 1420, 1998, 226-245.
• [12] Buchholz, P., Kemper, P.: Quantifying the dynamic behavior of process algebras, Lecture Notes in Computer Science, 2165, 2001, 184-199.
• [13] Buchholz, P., Tarasyuk, I. V.: A class of stochastic Petri nets with step semantics and related equivalence notions, Technische Berichte TUD-FI00-12, Fakultät Informatik, Technische Universität Dresden, Germany, November 2000, 18 pages, ftp://ftp.inf.tu-dresden.de/pub/berichte/tud00-12.ps.gz.
• [14] Buchholz, P., Tarasyuk, I. V.: Net and algebraic approaches to probablistic modeling, Joint Novosibirsk Computing Center and Institute of Informatics Systems Bulletin, Series Computer Science, 15, 2001, 31-64, Http://www.iis.nsk.su/persons/itar/spnpancc.pdf.
• [15] Devillers, R.: Petri boxes and finite processes, Lecture Notes in Computer Science, 1119, 1996, 465-480.
• [16] Donatelli, S., Ribaudo, M., Hillston, J.: A comparison of perfomance evaluation process algebra and generalized stochastic Petri nets, Proceedings of 6th International Workshop on Petri Nets and Performance Models, IEEE Computer Society Press, Durham, USA, 1995.
• [17] Florin, G., Natkin, S.: Les reseaux de Petri stochastiques, Technique et Science Informatique, 4(1), 1985.
• [18] van Glabbeek, R. J.: The linear time - branching time spectrum II: the semantics of sequential systems with silent moves. Extended abstract, Lecture Notes in Computer Science, 715, 1993, 66-81.
• [19] Hansson, H.: Time and probability in formal design of distributed systems, Real-Time Safety Critical Systems, 1, 1994.
• [20] Hermanns, H., Rettelbach, M.: Syntax, semantics, equivalences and axioms for MTIPP, Proceedings of 2nd Workshop on Process Algebras and Performance Modelling (U. Herzog, M. Rettelbach, Eds.), 27, University of Erlangen, Germany, 1994, Regensberg / Erlangen.
• [21] Hillston, J.: A compositional approach to performance modelling, Cambridge University Press, Great Britain, 1996.
• [22] Jonsson, B., Yi, W., Larsen, K. G.: Probabilistic extensions of process algebras, in: Handbook of Process Algebra (J. A. Bergstra, A. Ponse, S. A. Smolka, Eds.), chapter 11, Elsevier Science B.V., Amsterdam, The Netherlands, 2001, 685-710.
• [23] Kotov, V. E.: An algebra for parallelism based on Petri nets, Lecture Notes in Computer Science, 64, 1978, 39-55.
• [24] Kotov, V. E., Cherkasova, L. A.: On structural properties of generalized processes, Lecture Notes in Computer Science, 188, 1985, 288-306.
• [25] Koutny, M.: Partial order semantics of box expressions, Lecture Notes in Computer Science, 815, 1994, 318-337.
• [26] Koutny, M., Best, E.: Operational and denotational semantics for the box algebra, Theoretical Computer Science, 211(1-2), 1999, 1-83, Http://parsys.informatik.uni-oldenburg.de/˜best/publications/tcs.ps.gz.
• [27] Larsen, K. G., Skou, A.: Bisimulation through probabilistic testing, Information and Computation, 94(1), 1991, 1-28.
• [28] Larsen, K. G., Skou, A.: Compositional verification of probabilistic processes, Lecture Notes in Computer Science, 630, 1992, 456-471.
• [29] Macià, H. S.: sPBC: Una extensión Markoviana del Petri box calculus, Ph.D. Thesis, Department of Computer Science, University of Castilla-La Mancha, Albacete, Spain, 2003, In Spanish, http://www.infoab. uclm.es/fmc/publications/2003/sPBCthesis03.pdf.
• [30] Macià, H. S., Valero, R., V., Cuartero, F. G., Ruiz, M. C. D.: sPBC with immediate multiactions, July 2005, 27 pages, work in progress.
• [31] Macià, H. S., Valero, V. R., Cazorla, D. L., Cuartero, F. G.: Introducing the iteration in sPBC, Technical Report DIAB-03-01-37, Department of Computer Science, University of Castilla-La Mancha, Albacete, Spain, September 2003, 20 pages, http://www.info-ab.uclm.es/descargas/tecnicalreports/DIAB-03-01-37/diab030137.zip.
• [32] Macià, H. S., Valero, V. R., Cazorla, D. L., Cuartero, F. G.: Introducing the iteration in sPBC, Proceedings of the 24th International Conference on Formal Techniques for Networked and Distributed Systems - 04 (FORTE'04), Madrid, Spain, October 2004, Http://www.info-ab.uclm.es/fmc/publications/2004/forte04.pdf.
• [33] Macià, H. S., Valero, V. R., Cuartero, F. G.: A congruence relation in finite sPBC, Technical Report DIAB-02-01-31, Department of Computer Science, University of Castilla-La Mancha, Albacete, Spain, October 2002, 34 pages, http://www.info-ab.uclm.es/sec-ab/Tecrep/reportcong.pdf.
• [34] Macià, H. S., Valero, V. R., Cuartero, F. G.: Defining equivalence relations in sPBC, Proceedings of 1st International Conference on the Principles of Software Engineering - 04 (PriSE'04), Buenos Aires, Argentina, November 2004.
• [35] Macià, H. S., Valero, V. R., Cuartero, F. G., de Frutos, D. E.: A congruence relation for sPBC, June 2004, 62 pages, submitted.
• [36] Macià, H. S., Valero, V. R., Cuartero, F. G., Pelayo, F. L.: Improving the synchronization in stochastic Petri box calculus, Actas de las II Jornadas sobre Programacion y Lenguajes - 02 (PROLE'02), El Escorial, Spain, November 2002.
• [37] Macià, H. S., Valero, V. R., Cuartero, F. G., Pelayo, F. L.: A new proposal for the synchronization in sPBC, Technical Report DIAB-02-01-26, Department of Computer Science, University of Castilla-La Mancha, Albacete, Spain, June 2002, 15 pages, http://www.info-ab.uclm.es/sec-ab/Tecrep/newproposalsysPBC.ps.
• [38] Macià, H. S., Valero, V. R., Cuartero, F. G., Pelayo, F. L.: A new synchronization in finite stochastic Petri box calculus, Proceedings of 3rd International IEEE Conference on Application of Concurrency to System Design - 03 (ACSD'03), IEEE Computer Society Press, Guimar˜aes, Portugal, June 2003, Http://www.infoab.uclm.es/fmc/publications/2003/acsd03.pdf.
• [39] Macià, H. S., Valero, V. R., de Frutos, D. E.: sPBC: a Markovian extension of finite PBC, Actas de IX Jornadas de Concurrencia - 01 (JC'01), IEEE Computer Society Press, Sitges, Spain, June 2001, Http://www.info-ab.uclm.es/fmc/publications/2001/mvfjc01.ps.
• [40] Macià, H. S., Valero, V. R., de Frutos, D. E.: sPBC: a Markovian extension of finite Petri box calculus, Proceedings of 9th IEEE International Workshop on Petri Nets and Performance Models - 01 (PNPM'01), IEEE Computer Society Press, Aachen, Germany, September 2001, Http://www.infoab.uclm.es/fmc/publications/2001/pnpm01.ps.
• [41] Macià, H. S., Valero, V. R., de Frutos, D. E., Cuartero, F. G.: Extending PBC with Markovian multiactions, Proceedings of XXVII Conferencia Latinoamericana de Informática - 01 (CLEI'01), Universidad de los Andes, Mérida, Venezuela, September 2001, 12 pages, http://www.infoab.uclm.es/fmc/publications/2001/clei01.ps.
• [42] Milner, R. A. J.: Communication and concurrency, Prentice-Hall International, New York, USA, 1989.
• [43] Molloy, M.: Performance analysis using stochastic Petri nets, IEEE Transactions on Software Engineering, 31(9), 1982, 913-917.
• [44] Molloy, M.: Discrete time stochastic Petri nets, IEEE Transactions on Software Engineering, 11(4), 1985, 417-423.
• [45] Núñez, M.: An axiomatization of probabilistic testing, Lecture Notes in Computer Science, 1601, 1999, 130-150.
• [46] Núñez, M., de Frutos, D. E., Llana, L.: Acceptance trees for probabilistic processes, Lecture Notes in Computer Science, 962, 1995, 249-263.
• [47] Ribaudo, M.: Stochastic Petri net semantics for stochastic process algebra, Proceedings of 6th International Workshop on Petri Nets and Performance Models, IEEE Computer Society Press, Durham, NC, USA, 1995.
• [48] Tarasyuk, I. V.: Equivalence notions applied to designing concurrent systems with the use of Petri nets, Programming and Computer Software, 24(4), 1998, 162-175, Http://www.maik.rssi.ru/journals/procom.htm.
• [49] Tarasyuk, I. V.: Discrete time stochastic Petri box calculus, Berichte aus dem Department für Informatik 3/05, Carl von Ossietzky Universität Oldenburg, Germany, November 2005, 25 pages, http://www.iis.nsk.su/persons/itar/dtspbcib.pdf.