Abstract
Formal languages with semantics based on ordinary differential equations (ODEs) have emerged as a useful tool to reason about large-scale distributed systems. We present differential bisimulation, a behavioral equivalence developed as the ODE counterpart of bisimulations for languages with probabilistic or stochastic semantics. We study it in the context of a Markovian process algebra. Similarly to Markovian bisimulations yielding an aggregated Markov process in the sense of the theory of lumpability, differential bisimulation yields a partition of the ODEs underlying a process algebra term, whereby the sum of the ODE solutions of the same partition block is equal to the solution of a single (lumped) ODE. Differential bisimulation is defined in terms of two symmetries that can be verified only using syntactic checks. This enables the adaptation to a continuous-state semantics of proof techniques and algorithms for finite, discrete-state, labeled transition systems. For instance, we readily obtain a result of compositionality, and provide an efficient partition-refinement algorithm to compute the coarsest ODE aggregation of a model according to differential bisimulation.
This work was partially supported by the EU project QUANTICOL, 600708. The postdoctoral fellowship of G.I. is supported by CAPES. Part of this research has been carried out while the three authors were at University of Southampton, UK.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
All proofs are provided in the extended technical report [15].
- 2.
\(P. comp [\alpha ]\) is nil if \(\alpha \not \in \mathcal {A}(P)\), and free if \(\alpha \in \mathcal {A}(P)\) and \(\alpha \not \in \mathcal {D}(P,{\mathcal {M}})\), so to tell apart states performing different actions.
References
Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)
Bernardo, M.: A survey of Markovian behavioral equivalences. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 180–219. Springer, Heidelberg (2007)
Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31(1), 59–75 (1994)
Buchholz, P.: Markovian process algebra: composition and equivalence. In: Proceedings of 2nd PAPM Workshop. Erlangen, Germany (1994)
Camporesi, F., Feret, J.: Formal reduction for rule-based models. ENTCS 276, 29–59 (2011)
Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. TCS 410(33–34), 3065–3084 (2009)
Danos, V., Feret, J., Fontana, W., Harmer, R., Krivine, J.: Abstracting the differential semantics of rule-based models: exact and automated model reduction. In: LICS, pp. 362–381 (2010)
Danos, V., Laneve, C.: Formal molecular biology. TCS 325(1), 69–110 (2004)
Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309–315 (2003)
Haghverdi, E., Tabuada, P., Pappas, G.J.: Bisimulation relations for dynamical, control, and hybrid systems. TCS 342(2–3), 229–261 (2005)
Hayden, R.A., Bradley, J.T.: A fluid analysis framework for a Markovian process algebra. TCS 411(22–24), 2260–2297 (2010)
Hermanns, H., Rettelbach, M.: Syntax, semantics, equivalences, and axioms for MTIPP. In: Proceedings of Process Algebra and Probabilistic Methods, pp. 71–87. Erlangen (1994)
Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, p. 244. Springer, Heidelberg (1999)
Hillston, J.: A Compositional Approach to Performance Modelling, CUP. Cambridge University Press, New York (1996)
Iacobelli, G., Tribastone, M., Vandin, A.: Differential bisimulation for a Markovian process algebra. Extended Version. QUANTICOL TR-QC-04-2015 (2015). http://milner.inf.ed.ac.uk/wiki/files/W232G9A7/mfcs2015ExtendedTRpdf.html
Kurtz, T.G.: Solutions of ordinary differential equations as limits of pure jump Markov processes. J. Appl. Probab. 7(1), 49–58 (1970)
Kurtz, T.G.: Approximation of Population Processes, vol. 36. SIAM, Philadelphia (1981)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Okino, M.S., Mavrovouniotis, M.L.: Simplification of mathematical models of chemical reaction systems. Chem. Rev. 2(98), 391–408 (1998)
Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM 16(6), 973–989 (1987)
Pappas, G.J.: Bisimilar linear systems. Automatica 39(12), 2035–2047 (2003)
van der Schaft, A.J.: Equivalence of dynamical systems by bisimulation. IEEE TAC 49, 2160–2172 (2004)
Toth, J., Li, G., Rabitz, H., Tomlin, A.S.: The effect of lumping and expanding on kinetic differential equations. SIAM J. Appl. Math. 57(6), 1531–1556 (1997)
Tribastone, M., Gilmore, S., Hillston, J.: Scalable differential analysis of process algebra models. IEEE TSE 38(1), 205–219 (2012)
Tschaikowski, M., Tribastone, M.: A unified framework for differential aggregations in Markovian process algebra. JLAMP 84(2), 238–258 (2015)
Tschaikowski, M., Tribastone, M.: Exact fluid lumpability for Markovian process algebra. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 380–394. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Iacobelli, G., Tribastone, M., Vandin, A. (2015). Differential Bisimulation for a Markovian Process Algebra. In: Italiano, G., Pighizzini, G., Sannella, D. (eds) Mathematical Foundations of Computer Science 2015. MFCS 2015. Lecture Notes in Computer Science(), vol 9234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48057-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-662-48057-1_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48056-4
Online ISBN: 978-3-662-48057-1
eBook Packages: Computer ScienceComputer Science (R0)