### 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 language | English |
---|---|

Title of host publication | Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Proceedings |

Number of pages | 14 |

Volume | 9234 |

Publisher | Springer Verlag |

Publication date | 2015 |

Pages | 293-306 |

ISBN (Print) | 9783662480564 |

DOIs | |

Publication status | Published - 2015 |

Externally published | Yes |

Event | 40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015 - Milan, Italy Duration: 24 Aug 2015 → 28 Aug 2015 |

### Conference

Conference | 40th International Symposium on Mathematical Foundations of Computer Science, MFCS 2015 |
---|---|

Country | Italy |

City | Milan |

Period | 24/08/2015 → 28/08/2015 |

Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 9234 |

ISSN | 0302-9743 |

### Cite this

*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

}

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

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 -