Embeddings of hybrid automata in process algebra

Abstract

We study the expressive power of two modelling formalisms, viz. hybrid automata and μCRLt. The automaton based language of hybrid automata is a popular formalism that is used for describing and analysing the behaviours of hybrid systems. The process algebraic language μCRLt is designed for specifying real-time and data-dependent systems and to reason about such systems. We show that every hybrid automaton can be translated to a μCRLt expression without loss of information, i.e. the translation is equivalence preserving. This proves that μCRLt is at least as expressive as the modelling language of hybrid automata. Subsequently, we extend the standard model of a hybrid automaton to deal with communications via shared continuous variables. We show that the resulting enhanced hybrid automata can also be embedded in μCRLt. © Springer-Verlag 2004.