×

Logical characterization of fluid equivalences. (English) Zbl 1420.68148

Summary: 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 \(\mathrm{HML}_\mathrm{flt}\) and \(\mathrm{HML}_\mathrm{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.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
60J27 Continuous-time Markov processes on discrete state spaces
60K15 Markov renewal processes, semi-Markov processes
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] L. Aceto,Some of my favourite results in classic process algebra, Bulletin of the EATCS,81 (2003), 90-108. Zbl 1169.68533 · Zbl 1169.68533
[2] L. Aceto, D. Della Monica, I. F´abregas, A. Ing´olfsd´ottir,When are prime formulae characteristic?Lecture Notes in Computer Science,9234(2015), 76-88. Zbl 06482726 · Zbl 1425.68245
[3] A. Angius, A. Horv´ath, 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. Zbl 1392.68113 · Zbl 1392.68113
[4] C. Autant, W. Pfister, Ph. Schnoebelen,Place bisimulations for the reduction of labeled Petri nets with silent moves, Proc.6thInt. Conf. on Computing and Information (ICCI) 1994, Trent University, Peterborough, Ontario, Canada, May 1994, 230-246, 1994. http://www.lsv.enscachan.fr/Publis/PAPERS/PS/APS-icci94.ps
[5] C. Autant, Ph. Schnoebelen,Place bisimulations in Petri nets, Lecture Notes in Computer Science,616(1992), 45-61. MR1253088
[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. Zbl 1365.68313 · Zbl 1365.68313
[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. Zbl 1358.68181 · Zbl 1358.68181
[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. Zbl 0974.68017 · Zbl 0974.68017
[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.
[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. Zbl 1274.68264 · Zbl 1274.68264
[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. Zbl 1101.68053 · Zbl 1101.68053
[12] G. Balbo,Introduction to stochastic Petri nets, Lecture Notes in Computer Science,2090 (2001), 84-155. Zbl 0990.68092 · Zbl 0990.68092
[13] G. Balbo,Introduction to generalized stochastic Petri nets, Lecture Notes in Computer Science,4486(2007), 83-131. Zbl 1323.68400 · Zbl 1323.68400
[14] M. Bernardo,Markovian testing and trace equivalences exactly lump more than Markovian bisimilarity, Electronic Notes in Theoretical Computer Science,162(2006), 87-99. Zbl 1316.68086 · Zbl 1316.68086
[15] M. Bernardo,A survey of Markovian behavioral equivalences, Lecture Notes in Computer Science,4486(2007), 180-219. Zbl 1323.68402 · Zbl 1323.68402
[16] M. Bernardo,Non-bisimulation-based Markovian behavioral equivalences, Journal of Logic and Algebraic Programming,72(2007), 3-49. Zbl 1121.68077 · Zbl 1121.68077
[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. Zbl 1381.68195 · Zbl 1381.68195
[18] M. Bernardo, S. Botta,Modal logic characterization of Markovian testing and trace equivalences, Electronic Notes in Theoretical Computer Science,169(2006), 7-18. Zbl 1276.68119 · Zbl 1276.68119
[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. MR2459612 · Zbl 1141.68044
[20] M. Bernardo, R. Cleaveland,A theory of testing for Markovian processes, Lecture Notes in Computer Science,1877(2000), 305-319. Zbl 0999.68144 · Zbl 0999.68144
[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. Zbl 1358.68210 · Zbl 1358.68210
[22] M. Bernardo, L. Tesei,Encoding timed models as uniform labeled transition systems, Lecture Notes in Computer Science,8168(2013), 104-118.
[23] W.D. Blizard,The development of multiset theory, The Review of Modern Logic,1:4 (1991), 319-352. MR1112352 · Zbl 0744.03054
[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. Zbl 1286.68306 · Zbl 1286.68306
[25] A. Bobbio, S. Garg, M. Gribaudo, A. Horv´ath, M. Sereno, M. Telek,Modeling software systems with rejuvenation, restoration and checkpointing through fluid stochastic Petri nets, Proc.8thInt. Workshop on Petri Nets and Performance Models (PNPM) 1999, Zaragoza,
[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. MR1740521
[27] M. Boreale,Algebra, coalgebra, and minimization in polynomial differential equations, Lecture Notes in Computer Science,10203(2017), 71-87. Zbl 06720984 · Zbl 1486.68109
[28] P. Buchholz,A notion of equivalence for stochastic Petri nets, Lecture Notes in Computer Science,935(1995), 161-180. MR1461026 · Zbl 1496.68220
[29] P. Buchholz,Iterative decomposition and aggregation of labeled GSPNs, Lecture Notes in Computer Science,1420(1998), 226-245. · Zbl 1510.68053
[30] L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin,Forward and backward bisimulations for chemical reaction networks, Proc.26thInt. Conf. on Concurrency Theory (CONCUR) 2015, Madrid, Spain, September 2015, Leibniz International Proceedings in Informatics (LIPIcs),42(2015), 226-239. Zbl 1374.68204 · Zbl 1374.68204
[31] L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin,Symbolic computation of differential equivalences, Proc.43rdAnnual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2016, St. Petersburg, Florida, USA, January 2016, 137-150, ACM Press, 2016. http://sysma.imtlucca.it/wp-content/uploads/2015/11/z3-popl16.pdf Zbl 1347.68258 · Zbl 1347.68258
[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.
[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. · Zbl 1431.68072
[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. · Zbl 07703951
[35] G. Ciardo, J.K. Muppala, K.S. Trivedi,On the solution of GSPN reward models, Performance Evaluation,12:4 (1991), 237-253. Zbl 0754.60097 · Zbl 0754.60097
[36] G. Ciardo, D. Nicol, K.S. Trivedi,Discrete-event simulation of fluid stochastic Petri nets, Report,97-24, 15 p., Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center, Hampton, Virginia, USA, 1997. 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.
[38] G. Clark, S. Gimore, J. Hillston,Specifying performance measures for PEPA, Lecture Notes in Computer Science,1601(1999), 211-227.
[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. Zbl 0962.68120 · Zbl 0962.68120
[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. Zbl 1053.68065 · Zbl 1053.68065
[41] E.-E. Doberkrat,Congruences and bisimulations for continuous-time stochastic logic, Lecture Notes in Computer Science,3722(2005), 409-423. Zbl 1169.68503 · Zbl 1169.68503
[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.
[43] M. Gribaudo,Hybrid formalism for performance evaluation: theory and applications, Ph.D. thesis, 198 p., Department of Computer Science, University of Turin, Turin, Italy, 2002. http://www.di.unito.it/ marcog/Downloads/PhDThesis.pdf
[44] M. Gribaudo, A. Horv´ath,Fluid stochastic Petri nets augmented with flush-out arcs: a transient analysis technique, IEEE Transactions on Software Engineering,28:10 (2002), 944-955.
[45] M. Gribaudo, A. Horv´ath,Model checking functional and performability properties of stochastic fluid models, Electronic Notes in Theoretical Computer Science,128:6 (2005), 295-310. Zbl 1272.68251 · Zbl 1272.68251
[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. Zbl 1138.76012 · Zbl 1138.76012
[47] M. Gribaudo, M. Sereno,Simulation of fluid stochastic Petri nets, Proc.8thInt. Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS) 2000, San Francisco, USA, August 2000, 231-239, 2000. http://www.di.unito.it/  marcog/Downloads/MASCOTS00.pdf · Zbl 1510.68057
[48] M. Gribaudo, M. Sereno, A. Horv´ath, 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. Zbl 0972.93040 · Zbl 0972.93040
[49] M. Gribaudo, M. Telek,Fluid models in performance analysis, Lecture Notes in Computer Science,4486(2007), 271-317. Zbl 1323.68051 · Zbl 1323.68051
[50] M. Gribaudo, M. Telek,Stationary analysis of fluid level dependent bounded fluid models, Performance Evaluation,65:3-4 (2008), 241-261.
[51] B.R. Haverkort,Markovian models for performance and dependability evaluation, Lecture Notes in Computer Science,2090(2001), 38-83. Zbl 0990.68020 · Zbl 0990.68020
[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. MR0832336 · Zbl 0629.68021
[53] J. Hillston,A compositional approach to performance modelling, Cambridge University Press, Cambridge, UK, 1996. http://www.dcs.ed.ac.uk/pepa/book.pdf MR1427945 · Zbl 1080.68003
[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. Zbl 0957.90011 · Zbl 0957.90011
[55] A. Horv´ath, M. Gribaudo,Matrix geometric solution of fluid stochastic Petri nets, Proc. 4thInt. Conf. on Matrix-Analytic Methods in Stochastic Models (MAM) 2002, Adelaide, Australia, July 2002, 163-182, World Scientific, 2002. http://www.di.unito.it/ marcog/ Downloads/HoGr02.pdf Zbl 1162.93382 · Zbl 1162.93382
[56] G. Horv´ath, M. Telek,Matrix-analytic solution of infinite, finite and level-dependent secondorder fluid models, Queueing Systems — Theory and Applications,87:3-4 (2017), 325-343. Zbl 1377.60086 · Zbl 1377.60086
[57] G. Iacobelli, M. Tribastone, A. Vandin,Differential bisimulation for a Markovian process algebra, Lecture Notes in Computer Science,9234(2015), 293-306. Zbl 06482743 · Zbl 1465.68195
[58] V.G. Kulkarni,Modeling and analysis of stochastic systems. Second edition, Texts in Statistical Science,84, Chapman and Hall / CRC Press, 2009. Zbl 1191.60003
[59] K.G. Larsen, A. Skou,Bisimulation through probabilistic testing, Information and Computation,94:1 (1991), 1-28. Zbl 0756.68035 · Zbl 0756.68035
[60] M.A. Marsan,Stochastic Petri nets: an elementary introduction, Lecture Notes in Computer Science,424(1990), 1-29.
[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/ greatspn/GSPN-Wiley/ Zbl 0843.68080 · Zbl 0843.68080
[62] M.K. Molloy,Performance analysis using stochastic Petri nets, IEEE Transactions on Computing,31:9 (1982), 913-917.
[63] M.K. Molloy,Discrete time stochastic Petri nets, IEEE Transactions on Software Engineering, 11:4 (1985), 417-423. Zbl 0558.68053 · Zbl 0558.68053
[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).
[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. · Zbl 1514.68192
[66] A. Sharma,Trace relations and logical preservation for continuous-time Markov decision processes, Lecture Notes in Computer Science,10580(2017), 192-209. Zbl 06802664 · Zbl 1444.68122
[67] A. Sharma,Trace relations and logical preservation for Markov automata, Lecture Notes in Computer Science,11022(2018), 162-178. Zbl 06989605 · Zbl 1515.68167
[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. Zbl 06385877 · Zbl 1428.68191
[69] J. Sproston, S. Donatelli,Backward stochastic bisimulation in CSL model checking, Proc.1st Int. Conf. on the Quantitative Evaluation of Systems (QEST) 2004, 220-229, IEEE Computer Society Press, 2004. http://www.di.unito.it/ sproston/Research/qest04.ps.gz
[70] A. Syropoulos,Mathematics of multisets, Lecture Notes in Computer Science,2235(2001), 347-358. MR2054267 · Zbl 1052.03030
[71] I.V. Tarasyuk,Place bisimulation equivalences for design of concurrent and sequential systems, Electronic Notes in Theoretical Computer Science,18(1998), 191-206. MR1672359
[72] I.V. Tarasyuk,τ-equivalences and refinement for Petri nets based design, Technische Berichte, TUD-FI00-11, 41 p., Fakult¨at Informatik, Technische Universit¨at Dresden, Germany, 2000. http://itar.iis.nsk.su/files/itar/pages/eqtbrtud_cov.pdf, http://www.qucosa.de/fileadmin/ data/qucosa/documents/10037/tud_TB_2000-11.pdf
[73] I.V. Tarasyuk,Equivalences for behavioural analysis of concurrent and distributed computing systems, Academic Publisher “Geo”, Novosibirsk, 2007 (ISBN 978-5-9747-0098-9, in Russian).
[74] I.V. Tarasyuk, P. Buchholz,Bisimulation for fluid stochastic Petri nets, Bulletin of the Novosibirsk Computing Center, Series Computer Science, IIS Special Issue,38(2015), 121-149. Zbl 1374.68344 · Zbl 1374.68344
[75] I.V. Tarasyuk, P. Buchholz,Equivalences for fluid stochastic Petri nets, Siberian Electronic Mathematical Reports,14(2017), 317-366. Zbl 1373.68299 · Zbl 1373.68299
[76] K.S. Trivedi, V.G. Kulkarni,FSPNs: fluid stochastic Petri nets, Lecture Notes in Computer Science,691(1993), 24-31.
[77] M. Tribastone, A. Vandin,Speeding up stochastic and deterministic simulation by aggregation: an advanced tutorial, Proc. the 2018 Winter Simulation Conf. (WSC) 2018 (M. Rabe, A. Skoogh, N. Mustafee, A.A. Juan, eds.), Gothenburg, Sweeden, December 2018, 15 p., IEEE Computer Society Press, 2018. http://cse.lab.imtlucca.it/ mirco.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. Zbl 1364.68297 · Zbl 1364.68297
[79] M. Tschaikowski, M. Tribastone,Exact fluid lumpability in Markovian process algebra, Theoretical Computer Science,538(2014), 140-166. Zbl 1359.68228 · Zbl 1359.68228
[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. Zbl 1319.68151 · Zbl 1319.68151
[81] M. Tschaikowski, M. Tribastone,Approximate reduction of heterogenous nonlinear models with differential hulls, IEEE Transactions on Automatic Control,61:4 (2016), 1099-1104. Zbl 1359.93084 · Zbl 1359.93084
[82] V. Wolf,Testing theory for probabilistic processes, Lecture Notes in Computer Science,347 (2005), 233-275.
[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.
[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.
[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,1stWorld Congress on Systems Simulation (WCSS) 1997, Singapore, September 1997, 328-332, IEEE Singapore Section, Singapore, 1997. http://page.mi.fu-berlin.de/katinkaw/ publications/anmt
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.