Differential bisimulation for a Markovian process algebra

Giulio Iacobelli, Mirco Tribastone*, Andrea Vandin

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.

Original languageEnglish
Title of host publicationMathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings
Number of pages14
Volume9234
PublisherSpringer Verlag
Publication date2015
Pages293-306
ISBN (Print)9783662480564
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015 - Milan, Italy
Duration: 24 Aug 201528 Aug 2015

Conference

Conference40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015
CountryItaly
CityMilan
Period24/08/201528/08/2015
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9234
ISSN0302-9743

Cite this

Iacobelli, G., Tribastone, M., & Vandin, A. (2015). Differential bisimulation for a Markovian process algebra. In Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings (Vol. 9234, pp. 293-306). Springer Verlag. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol.. 9234 https://doi.org/10.1007/978-3-662-48057-1_23
Iacobelli, Giulio ; Tribastone, Mirco ; Vandin, Andrea. / Differential bisimulation for a Markovian process algebra. Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings. Vol. 9234 Springer Verlag, 2015. pp. 293-306 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9234).
@inproceedings{d32af4d50b1042c5a58c00a0736e0295,
title = "Differential bisimulation for a Markovian process algebra",
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.",
author = "Giulio Iacobelli and Mirco Tribastone and Andrea Vandin",
year = "2015",
doi = "10.1007/978-3-662-48057-1_23",
language = "English",
isbn = "9783662480564",
volume = "9234",
pages = "293--306",
booktitle = "Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings",
publisher = "Springer Verlag",
address = "Germany",

}

Iacobelli, G, Tribastone, M & Vandin, A 2015, Differential bisimulation for a Markovian process algebra. in Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings. vol. 9234, Springer Verlag, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9234, pp. 293-306, 40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015, Milan, Italy, 24/08/2015. https://doi.org/10.1007/978-3-662-48057-1_23

Differential bisimulation for a Markovian process algebra. / Iacobelli, Giulio; Tribastone, Mirco; Vandin, Andrea.

Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings. Vol. 9234 Springer Verlag, 2015. p. 293-306 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9234).

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Differential bisimulation for a Markovian process algebra

AU - Iacobelli, Giulio

AU - Tribastone, Mirco

AU - Vandin, Andrea

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-48057-1_23

DO - 10.1007/978-3-662-48057-1_23

M3 - Article in proceedings

SN - 9783662480564

VL - 9234

SP - 293

EP - 306

BT - Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings

PB - Springer Verlag

ER -

Iacobelli G, Tribastone M, Vandin A. Differential bisimulation for a Markovian process algebra. In Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings. Vol. 9234. Springer Verlag. 2015. p. 293-306. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9234). https://doi.org/10.1007/978-3-662-48057-1_23