Geodesic
Logical characterization of fluid equivalences
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 16 (2019), pp. 826-862.

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

We investigate fluid equivalences that allow one to compare and reduce behaviour of labeled fluid stochastic Petri nets (LFSPNs) with a single continuous place while preserving their discrete and continuous properties. We propose a linear-time relation of fluid trace equivalence and its branching-time counterpart, fluid bisimulation equivalence. Both fluid relations take into account 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. Moreover, we 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 characterize logically fluid trace and bisimulation equivalences with two novel fluid modal logics $HML_{flt}$ and $HML_{flb}$, constructed on the basis of the well-known Hennessy-Milner Logic (HML). These characterizations guarantee that two LFSPNs are fluid (trace or bisimulation) equivalent iff they satisfy the same formulas of the respective logic, i.e. they are logically equivalent. The results imply operational characterizations of the logical equivalences.
Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid model, transient and stationary behaviour, fluid trace and bisimulation equivalences, fluid modal logic, logical and operational characterizations. 
@article{SEMR_2019_16_a13,
     author = {I. V. Tarasyuk and P. Buchholz},
     title = {Logical characterization of fluid equivalences},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {826--862},
     publisher = {mathdoc},
     volume = {16},
     year = {2019},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/}
}
TY  - JOUR
AU  - I. V. Tarasyuk
AU  - P. Buchholz
TI  - Logical characterization of fluid equivalences
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2019
SP  - 826
EP  - 862
VL  - 16
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/
LA  - en
ID  - SEMR_2019_16_a13
ER  - 
%0 Journal Article
%A I. V. Tarasyuk
%A P. Buchholz
%T Logical characterization of fluid equivalences
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2019
%P 826-862
%V 16
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/
%G en
%F SEMR_2019_16_a13
I. V. Tarasyuk; P. Buchholz. Logical characterization of fluid equivalences. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 16 (2019), pp. 826-862. http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/

[1] L. Aceto, “Some of my favourite results in classic process algebra”, Bulletin of the EATCS, 81 (2003), 90–108 | MR | Zbl

[2] L. Aceto, D. Della Monica, I. Fábregas, A. Ingólfsdóttir, When are prime formulae characteristic?, Lecture Notes in Computer Science, 9234, 2015, 76–88 | DOI | MR | Zbl

[3] A. Angius, A. Horváth, S.M. Halawani, O. Barukab, A.R. Ahmad, G. Balbo, “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 | Zbl

[4] C. Autant, W. Pfister, Ph. Schnoebelen, “Place bisimulations for the reduction of labeled Petri nets with silent moves”, Proc. $6^{th}$ Int. Conf. on Computing and Information (ICCI) 1994 (Trent University, Peterborough, Ontario, Canada, May 1994), 1994, 230–246 http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/APS-icci94.ps | MR

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

[6] A. Aziz, K. Sanwal, V. Singhal, R. Brayton, “Model checking continuous time Markov chains”, ACM Transactions on Computational Logic,, 1:1 (2000), 162–170 | DOI | MR | Zbl

[7] C. Baier, E.M. Hahn, B.R. Haverkort, H. Hermanns, J.-P. Katoen, “Model checking for performability”, Mathematical Structures in Computer Science, 23:4 (2013), 751–795 | DOI | MR | Zbl

[8] C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen, “Model checking continuous-time Markov chains by transient analysis”, Lecture Notes in Computer Science, 1855, 2000, 358–372 | DOI | MR | Zbl

[9] C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen, “Model-checking algorithms for continuous-time Markov chains”, IEEE Transactions on Software Engineering, 29:6 (2003), 524–541 | DOI | MR

[10] C. Baier, H. Hermanns, J.-P. Katoen, V. Wolf, “Comparative branching-time semantics for Markov chains”, Lecture Notes in Computer Science, 2761, 2003, 492–507 | DOI | MR | Zbl

[11] C. Baier, J.-P. Katoen, H. Hermanns, V. Wolf, “Comparative branching-time semantics for Markov chains”, Information and Computation, 200:2 (2005), 149–214 | DOI | MR | Zbl

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

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

[14] M. Bernardo, “Markovian testing and trace equivalences exactly lump more than Markovian bisimilarity”, Electronic Notes in Theoretical Computer Science, 162 (2006), 87–99 | DOI | Zbl

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

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

[17] M. Bernardo, “ULTraS at work: compositionality metaresults for bisimulation and trace semantics”, Journal of Logical and Algebraic Methods in Programming, 94 (2018), 150–182 | DOI | MR | Zbl

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

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

[20] M. Bernardo, R. Cleaveland, “A theory of testing for Markovian processes”, Lecture Notes in Computer Science, 1877, 2000, 305–319 | DOI | MR | Zbl

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

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

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

[24] S. Blom, B.R. Haverkort, M. Kuntz, J. van de Pol,, “Distributed Markovian bisimulation reduction aimed at CSL model checking”, Electronic Notes in Theoretical Computer Science,, 220:2 (2008), 35–50 | DOI | Zbl

[25] A. Bobbio, S. Garg, M. Gribaudo, A. Horváth, M. Sereno, M. Telek, “Modeling software systems with rejuvenation, restoration and checkpointing through fluid stochastic Petri nets”, Proc. $8^{th}$ Int. Workshop on Petri Nets and Performance Models (PNPM) 1999 (Zaragoza, Spain, September 1999), IEEE Computer Society Press, 1999, 82–91 \href{http://www.di.unito.it/~marcog/Downloads/PNPM99-BGGHST.pdf}http://www.di.unito.it/m̃arcog/Downloads/PNPM99-BGGHST.pdf

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

[27] M. Boreale, “Algebra, coalgebra, and minimization in polynomial differential equations”, Lecture Notes in Computer Science, 10203, 2017, 71–87 | DOI | MR | Zbl

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

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

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

[31] L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin, “Symbolic computation of differential equivalences”, Proc. $43^{rd}$ Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2016 (St. Petersburg, Florida, USA, January 2016), ACM Press, 2016, 137–150 http://sysma.imtlucca.it/wp-content/uploads/2015/11/z3-popl16.pdf | DOI | Zbl

[32] L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin, “Maximal aggregation of polynomial dynamical systems”, Proceedings the National Academy of Sciences of the United States of America, 114:38 (2017), 10029–10034 | DOI

[33] L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin, “Syntactic Markovian bisimulation for chemical reaction networks”, Lecture Notes in Computer Science, 10460, 2017, 466–483 | DOI | MR

[34] L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin, “Guaranteed error bounds on approximate model abstractions through reachability analysis”, Lecture Notes in Computer Science, 11024, 2018, 104–121 | DOI

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

[36] G. Ciardo, D. Nicol, K.S. Trivedi, 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, 1997, 15 pp. http://historical.ncstrl.org/tr/pdf/icase/TR-97-24.pdf

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

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

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

[40] J. Desharnais, P. Panangaden, “Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes”, Journal of Logic and Algebraic Programming, 56:1–2 (2003), 99–115 | DOI | MR | Zbl

[41] E.-E. Doberkrat, “Congruences and bisimulations for continuous-time stochastic logic”, Lecture Notes in Computer Science, 3722, 2005, 409–423 | DOI | MR | Zbl

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

[43] M. Gribaudo, Hybrid formalism for performance evaluation: theory and applications, Ph.D. thesis, Department of Computer Science, University of Turin, Turin, Italy, 2002, 198 pp. http://www.di.unito.it/m̃arcog/Downloads/PhDThesis.pdf

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

[45] M. Gribaudo, A. Horváth, “Model checking functional and performability properties of stochastic fluid models”, Electronic Notes in Theoretical Computer Science, 128:6 (2005), 295–310 | DOI | Zbl

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

[47] M. Gribaudo, M. Sereno, “Simulation of fluid stochastic Petri nets”, Proc. $8^{th}$ Int. Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS) 2000 (San Francisco, USA, August 2000), 2000, 231–239 http://www.di.unito.it/m̃arcog/Downloads/MASCOTS00.pdf | DOI

[48] M. Gribaudo, M. Sereno, A. Horváth, A. Bobbio, “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

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

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

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

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

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

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

[55] A. Horváth, M. Gribaudo, “Matrix geometric solution of fluid stochastic Petri nets”, Proc. $4^{th}$ Int. Conf. on Matrix-Analytic Methods in Stochastic Models (MAM) 2002 (Adelaide, Australia, July 2002), World Scientific, 2002, 163–182 http://www.di.unito.it/m̃arcog/Downloads/HoGr02.pdf | Zbl

[56] G. Horváth, M. Telek, “Matrix-analytic solution of infinite, finite and level-dependent second-order fluid models”, Queueing Systems — Theory and Applications, 87:3–4 (2017), 325–343 | DOI | MR | Zbl

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

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

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

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

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

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

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

[64] S.O. Natkin, 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 (in French) | MR

[65] M.R. Pedersen, G. Bacci, K.G. Larsen, R. Mardare, “A hemimetric extension of simulation for semi-Markov decision processes”, Lecture Notes in Computer Science, 11024, 2018, 339–355 | DOI

[66] A. Sharma, “Trace relations and logical preservation for continuous-time Markov decision processes”, Lecture Notes in Computer Science, 10580, 2017, 192–209 | DOI | MR | Zbl

[67] A. Sharma, “Trace relations and logical preservation for Markov automata”, Lecture Notes in Computer Science, 11022, 2018, 162–178 | DOI | MR | Zbl

[68] L. Song, L. Zhang, J.C. Godskesen, “Bisimulations and logical characterizations on continuous-time Markov decision processes”, Lecture Notes in Computer Science, 8318, 2014, 98–117 | DOI | MR | Zbl

[69] J. Sproston, S. Donatelli, “Backward stochastic bisimulation in CSL model checking”, Proc. $1^{st}$ Int. Conf. on the Quantitative Evaluation of Systems (QEST) 2004, IEEE Computer Society Press, 2004, 220–229 http://www.di.unito.it/s̃proston/Research/qest04.ps.gz

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

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

[72] I.V. Tarasyuk, $\tau$-equivalences and refinement for Petri nets based design, Technische Berichte, TUD-FI00-11, Fakultät Informatik, Technische Universität Dresden, Germany, 2000, 41 pp. ; http://www.qucosa.de/fileadmin/data/qucosa/documents/10037/tud_TB_2000-11.pdfhttp://itar.iis.nsk.su/files/itar/pages/eqtbrtud_cov.pdf

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

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

[75] I.V. Tarasyuk, P. Buchholz, “Equivalences for fluid stochastic Petri nets”, Siberian Electronic Mathematical Reports, 14 (2017), 317–366 | MR | Zbl

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

[77] M. Tribastone, A. Vandin,, “Speeding up stochastic and deterministic simulation by aggregation: an advanced tutorial”, Proc. the 2018 Winter Simulation Conf. (WSC) (Gothenburg, Sweeden, December 2018), eds. M. Rabe, A. Skoogh, N. Mustafee, A.A. Juan, IEEE Computer Society Press, 2018, 15 pp. http://cse.lab.imtlucca.it/m̃irco.tribastone/papers/wsc18.pdf

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

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

[80] M. Tschaikowski, M. Tribastone, “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

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

[82] V. Wolf, “Testing theory for probabilistic processes”, Lecture Notes in Computer Science, 347, 2005, 233–275 | DOI

[83] V. Wolf, C. Baier, M. Majster-Cederbaum,, “Trace machines for observing continuous-time Markov chains”, Electronic Notes in Theoretical Computer Science, 153:2 (2006), 259–277 | DOI

[84] V. Wolf, C. Baier, M. Majster-Cederbaum,, “Trace semantics for stochastic systems with nondeterminism”, Electronic Notes in Theoretical Computer Science,, 164:3 (2006), 187–204 | DOI

[85] K. Wolter, “Second order fluid stochastic Petri nets: an extension of GSPNs for approximate and continuous modelling”, Proc. Workshop on Analytical and Numerical Modelling Techniques, $1^{st}$ World Congress on Systems Simulation (WCSS) 1997 (Singapore, September 1997), IEEE Singapore Section, Singapore, 1997, 328–332 http://page.mi.fu-berlin.de/katinkaw/publications/anmt.ps