Equivalences for fluid stochastic Petri nets

I. V. Tarasyuk ; P. Buchholz

Sibirskie èlektronnye matematičeskie izvestiâ, Tome 14 (2017), pp. 317-366.

Résumé

We propose fluid equivalences to compare and reduce behaviour of labeled fluid stochastic Petri nets (LFSPNs) while preserving their discrete and continuous properties. We define a linear-time relation of fluid trace equivalence and its branching-time counterpart, fluid bisimulation equivalence. Both fluid relations respect the essential features of the LFSPNs behaviour, such as functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose continuous markings have no influence to the discrete ones, i.e. every discrete marking determines completely both the set of enabled transitions, their firing rates and the fluid flow rates of the incoming and outgoing arcs for each continuous place. We also require that the discrete part of the LFSPNs should be continuous time stochastic Petri nets. The underlying stochastic model for the discrete part of the LFSPNs is continuous time Markov chains (CTMCs). The performance analysis of the continuous part of LFSPNs is accomplished via the associated stochastic fluid models (SFMs). We show that fluid trace equivalence preserves average potential fluid change volume for the transition sequences of every certain length. We prove that fluid bisimulation equivalence preserves the following aggregated (by such a bisimulation) probability functions: stationary probability mass for the underlying CTMC, as well as stationary fluid buffer empty probability, fluid density and distribution for the associated SFM. Fluid bisimulation equivalence is then used to simplify the qualitative and quantitative analysis of LFSPNs that is accomplished by means of quotienting (by the equivalence) the discrete reachability graph and underlying CTMC. The application example of a document preparation system demonstrates the behavioural analysis via quotienting by fluid bisimulation equivalence.

Détail

Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid model, transient and stationary behaviour, buffer empty probability, fluid density and distribution, performance analysis, fluid trace and bisimulation equivalences
Mots-clés : Markovian trace and bisimulation equivalences, quotient, application.

Bibliographie

[1] Angius A., Horváth A., Halawani S. M., Barukab O., Ahmad A. R., Balbo G., “Use of flow equivalent servers in the transient analysis of product form queueing networks”, Lecture Notes in Computer Science, 9081, 2015, 15–29 | DOI | MR

[2] Autant C., Pfister W., Schnoebelen Ph., “Place bisimulations for the reduction of labeled Petri nets with silent moves”, Proceedings of $6^{th}$ International Conference on Computing and Information-94, ICCI'94, Trent University, Canada, 2014, 230–246 http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APS-icci94.ps | MR

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

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

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

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

[7] Bernardo M., “Non-bisimulation-based Markovian behavioral equivalences”, Journal of Logic and Algebraic Programming, 72 (2007), 3–49 | DOI | MR | Zbl

[8] Bernardo M., Botta S., “Modal logic characterization of Markovian testing and trace equivalences”, Proceedings of $1^{st}$ International Workshop on Logic, Models and Computer Science-06 (Camerino, Italy, April 2006), Electronic Notes in Theoretical Computer Science, 169, eds. F. Corradini, C. Toffalori, 2006, 7–18 | DOI | MR

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

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

[11] Bernardo M., Tesei L., “Encoding timed models as uniform labeled transition systems”, Lecture Notes in Computer Science, 8168, 2013, 104–118 | DOI

[12] Blizard W. D., “The development of multiset theory”, The Review of Modern Logic, 1:4 (1991), 319–352 | MR | Zbl

[13] Bobbio A., Garg S., Gribaudo M., Horváth A., Sereno M., Telek M., “Modeling software systems with rejuvenation, restoration and checkpointing through fluid stochastic Petri nets”, Proceedings of $8^{th}$ International Workshop on Petri Nets and Performance Models-99, PNPM'99 (Zaragoza, Spain, September 1999), IEEE Computer Society Press, 82–91 | MR

[14] Bobbio A., Puliafito A., Telek M., Trivedi K. S., “Recent developments in non-Markovian stochastic Petri nets”, Journal of Circuits, Systems and Computers, 8:1 (1998), 119–158 | DOI | MR

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

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

[17] Cardelli L., Tribastone M., Tschaikowski M., Vandin A., “Forward and backward bisimulations for chemical reaction networks”, Proceedings of $26^{th}$ International Conference on Concurrency Theory-15, CONCUR'15 (Madrid, Spain, September 2015), Leibniz International Proceedings in Informatics (LIPIcs), 42, 2015, 226–239 | MR

[18] Cardelli L., Tribastone M., Tschaikowski M., Vandin A., “Comparing chemical reaction networks: a categorical and algorithmic perspective”, Proceedings of $31^{st}$ Annual ACM/IEEE Symposium on Logic in Computer Science-16, LICS'16 (New York, USA, July 2016), ACM Press, 2016, 13 pp. | Zbl

[19] Cardelli L., Tribastone M., Tschaikowski M., Vandin A., “Symbolic computation of differential equivalences”, Proceedings of $43^{rd}$ Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages-16, POPL'16 (St. Petersburg, January 2016), ACM Press, Florida, USA, 2016, 137–150 | Zbl

[20] Cardelli L., Tribastone M., Tschaikowski M., Vandin A., “Efficient syntax-driven lumping of differential equations”, Lecture Notes in Computer Science, 9636, 2016, 93–111 | DOI

[21] Ciardo G., Muppala J. K., Trivedi K. S., “On the solution of GSPN reward models”, Performance Evaluation, 12:4 (1991), 237–253 | DOI | MR | Zbl

[22] Ciardo G., Nicol D., Trivedi K. S., Discrete-event simulation of fluid stochastic Petri nets, Report, 97-24, Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, Virginia, USA, May 1997, 15 pp.

[23] Ciardo G., Nicol D., Trivedi K. S., “Discrete-event simulation of fluid stochastic Petri nets”, IEEE Transactions on Software Engineering, 25:2 (1999), 207–217 | DOI

[24] Clark G., Gimore S., Hillston J., “Specifying performance measures for PEPA”, Lecture Notes in Computer Science, 1601, 1999, 211–227 | DOI

[25] Clark G., Gilmore S., Hillston J., Ribaudo M., “Exploiting modal logic to express performance measures”, Lecture Notes in Computer Science, 1786, 2000, 247–261 | DOI | Zbl

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

[27] Elwalid A. I., Mitra D., “Statistical multiplexing with loss priorities in rate-based congestion control of high-speed networks”, IEEE Transactions on Communications, 42:11 (1994), 2989–3002 | DOI

[28] Gribaudo M., Hybrid formalism for performance evaluation: theory and applications, Ph.D. thesis, Department of Computer Science, University of Turin, Turin, Italy, 2002, 198 pp.

[29] Gribaudo M., Horváth A., “Fluid stochastic Petri nets augmented with flush-out arcs: a transient analysis technique”, IEEE Transactions on Software Engineering, 28:10 (2002), 944–955 | DOI

[30] Gribaudo M., Manini D., Sericola B., Telek M., “Second order fluid models with general boundary behaviour”, Annals of Operations Research, 160 (2008), 69–82 | DOI | MR | Zbl

[31] Gribaudo M., Sereno M., “Simulation of fluid stochastic Petri nets”, Proceedings of $8^{th}$ International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems-00, MASCOTS'00, 2000, 231–239

[32] Gribaudo M., Sereno M., Horváth A., Bobbio A., “Fluid stochastic Petri nets augmented with flush-out arcs: modelling and analysis”, Discrete Event Dynamic Systems: Theory and Applications, 11:1–2 (2001), 97–117 | DOI | MR | Zbl

[33] Gribaudo M., Telek M., “Fluid models in performance analysis”, Lecture Notes in Computer Science, 4486, 2007, 271–317 | DOI | Zbl

[34] Gribaudo M., Telek M., “Stationary analysis of fluid level dependent bounded fluid models”, Performance Evaluation, 65:3–4 (2008), 241–261 | DOI

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

[36] Hayden R. A., Bradley J. T., “A fluid analysis framework for a Markovian process algebra”, Theoretical Computer Science, 411 (2010), 2260–2297 | DOI | MR | Zbl

[37] Hennessy M. C. B., Milner R. A. J., “Algebraic laws for non-determinism and concurrency”, Journal of the ACM, 32:1 (1985), 137–161 | DOI | MR | Zbl

[38] Hillston J., A compositional approach to performance modelling, Cambridge University Press, UK, 1996 | MR

[39] Horton G., Kulkarni V. G., Nicol D. M., Trivedi K. S., “Fluid stochastic Petri nets: theory, applications, and solution techniques”, European Journal of Operations Research, 105:1 (1998), 184–201 | DOI | Zbl

[40] Horváth A., Gribaudo M., “Matrix geometric solution of fluid stochastic Petri nets”, Proceedings of $4^{th}$ International Conference on Matrix-Analytic Methods in Stochastic Models-02, 2002, 163–182 | MR | Zbl

[41] Iacobelli G., Tribastone M., Vandin A., “Differential bisimulation for a Markovian process algebra”, Lecture Notes in Computer Science, 9234, 2015, 293–306 | DOI | MR | Zbl

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

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

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

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

[46] Molloy M. K., “Performance analysis using stochastic Petri nets”, IEEE Transactions on Computing, 31:9 (1982), 913–917 | DOI

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

[48] Natkin S. O., Les reseaux de Petri stochastiques et leur application a l'evalution des systemes informatiques, Ph. D. thesis, Conseratoire National des Arts et Metiers, France, 1980

[49] Syropoulos A., “Mathematics of multisets”, Lecture Notes in Computer Science, 2235, 2001, 347–358 | DOI | MR | Zbl

[50] Tarasyuk I. V., “Place bisimulation equivalences for design of concurrent and sequential systems”, Electronic Notes in Theoretical Computer Science, 18 (1998), 191–206 | DOI | MR

[51] Tarasyuk I. V., $\tau$-equivalences and refinement for Petri nets based design, Technische Berichte, TUD-FI00-11, Fakultät Informatik, Technische Universität Dresden, Germany, 2000

[52] Tarasyuk I. V., Equivalences for behavioural analysis of concurrent and distributed computing systems, Academic Publisher “Geo”, Novosibirsk, 2007 (in Russian)

[53] Tarasyuk I. V., Buchholz P., “Bisimulation for fluid stochastic Petri nets”, Bulletin of the Novosibirsk Computing Center, Series Computer Science, 38, IIS Special Issue (2015), 121–149

[54] Tóth J., Li G., Rabitz H., Tomlin A. S., “The effect of lumping and expanding on kinetic differential equations”, SIAM Journal of Applied Mathematics, 57:6 (1997), 1531–1556 | DOI | MR | Zbl

[55] Trivedi K. S., Kulkarni V. G., “FSPNs: fluid stochastic Petri nets”, Lecture Notes in Computer Science, 691, 1993, 24–31 | DOI

[56] Tschaikowski M., Tribastone M., “Exact fluid lumpability for Markovian process algebra”, Lecture Notes in Computer Science, 7454, 2012, 380–394 | DOI | MR | Zbl

[57] Tschaikowski M., Tribastone M., “Tackling continuous state-space explosion in a Markovian process algebra”, Theoretical Computer Science, 517 (2014), 1–33 | DOI | MR | Zbl

[58] Tschaikowski M., Tribastone M., “Exact fluid lumpability in Markovian process algebra”, Theoretical Computer Science, 538 (2014), 140–166 | DOI | MR | Zbl

[59] Tschaikowski M., Tribastone M., “Extended differential aggregations in process algebra for performance and biology”, Proceedings of $12^{th}$ International Workshop on Quantitative Aspects of Programming Languages and Systems-14 (QAPL'14) (Grenoble, France, April 2014), Electronic Proceedings in Theoretical Computer Science, 154, 2014, 34–47 | DOI

[60] Tschaikowski M., Tribastone M., “A unified framework for differential aggregations in Markovian process algebra”, Journal of Logical and Algebraic Methods in Programming, 84 (2015), 238–258 | DOI | MR | Zbl

[61] Tschaikowski M., Tribastone M., “Approximate reduction of heterogenous nonlinear models with differential hulls”, IEEE Transactions on Automatic Control, 61:4 (2016), 1099–1104 | DOI | MR

[62] Wolf V., Baier C., Majster-Cederbaum M., “Trace machines for observing continuous-time Markov chains”, Proceedings of $3^{rd}$ International Workshop on Quantitative Aspects of Programming Languages-05 (QAPL'05) (Edinburgh, UK, 2005), Electronic Notes in Theoretical Computer Science, 153, no. 2, 2006, 259–277 | DOI

[63] Wolter K., “Second order fluid stochastic Petri nets: an extension of GSPNs for approximate and continuous modelling”, Proceedings of Workshop on Analytical and Numerical Modelling Techniques, $1^{st}$ World Congress on Systems Simulation-97, 1997, 328–332