Embeddings of hybrid automata in process algebra

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
2 Downloads (Pure)

Abstract

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 .
Original languageEnglish
Title of host publicationIntegrated Formal Methods (Proceedings IFM 2004, Canterbury, UK, April 4-7, 2004)
EditorsE. Boiten, J. Derrick, G. Smith
Place of PublicationBerlin
PublisherSpringer
Pages343-362
ISBN (Print)3-540-21377-5
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
Volume2999
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Embeddings of hybrid automata in process algebra'. Together they form a unique fingerprint.

Cite this