Bisimulation Relations Between Automata, Stochastic Differential Equations and Petri Nets

Mariken H.C. Everdij
(National Aerospace Laboratory NLR, NL)
Henk A.P. Blom
(National Aerospace Laboratory NLR, NL)

Two formal stochastic models are said to be bisimilar if their solutions as a stochastic process are probabilistically equivalent. Bisimilarity between two stochastic model formalisms means that the strengths of one stochastic model formalism can be used by the other stochastic model formalism. The aim of this paper is to explain bisimilarity relations between stochastic hybrid automata, stochastic differential equations on hybrid space and stochastic hybrid Petri nets. These bisimilarity relations make it possible to combine the formal verification power of automata with the analysis power of stochastic differential equations and the compositional specification power of Petri nets. The relations and their combined strengths are illustrated for an air traffic example.

In Manuela Bujorianu and Michael Fisher: Proceedings FM-09 Workshop on Formal Methods for Aerospace (FMA 2009), Eindhoven, The Netherlands, 3rd November 2009, Electronic Proceedings in Theoretical Computer Science 20, pp. 1–15.
Published: 28th March 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.20.1 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org