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


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
PublisherSpringer Verlag
Publication date2015
ISBN (Print)9783662480564
Publication statusPublished - 2015
Externally publishedYes
Event40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015 - Milan, Italy
Duration: 24 Aug 201528 Aug 2015


Conference40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)


Dive into the research topics of 'Differential bisimulation for a Markovian process algebra'. Together they form a unique fingerprint.

Cite this