Embeddings of hybrid automata in process algebra

We study the expressive power of two modelling formalisms, viz. hybrid automata and muCRL(t). 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 muCRL(t) 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 muCRL(t) expression without loss of information, i.e. the translation is equivalence preserving. This proves that muCRL(t) 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 muCRL(t).