We study the expressive power of two modelling formalisms, viz. hybrid automata and µCRL 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 µCRL 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 µCRL t expression without loss of information, i.e. the translation is equivalence preserving. This proves that µCRL 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 µCRL t .
|Title of host publication||Integrated Formal Methods (Proceedings IFM 2004, Canterbury, UK, April 4-7, 2004)|
|Editors||E. Boiten, J. Derrick, G. Smith|
|Place of Publication||Berlin|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science|