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

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

Cite this