Conference paper
Differential Bisimulation for a Markovian Process Algebra
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.
Language: | English |
---|---|
Publisher: | Springer Berlin Heidelberg |
Year: | 2015 |
Pages: | 293-306 |
Proceedings: | International Symposium on Mathematical Foundations of Computer Science |
ISBN: | 3662480565 , 3662480573 , 9783662480564 and 9783662480571 |
Types: | Conference paper |
DOI: | 10.1007/978-3-662-48057-1_23 |