Computing Publications

Publications Home » Denotational Semantics of Hybrid ...

Denotational Semantics of Hybrid Automata

Abbas Edalat, Dirk Pattinson

Conference or Workshop Paper
Foundations of Software Science and Computation Structures: 9th International Conference, FOSSACS 2006
March, 2006
Lecture Notes in Computer Science
Volume 3921
pp.231–245
ISBN 3-540-33045-3
Abstract

We introduce a denotational semantics for non-linear hybrid automata, and relate it to the operational semantics given in terms of hybrid trajectories. The semantics is defined as least fixpoint of an operator on the continuous domain of functions of time that take values in the lattice of compact subsets of n-dimensional Euclidean space. The semantic function assigns to every point in time the set of states the automaton can visit at that time, starting from one of its initial states. Our main results are the correctness and computational adequacy of the denotational semantics with respect to the operational semantics and the fact that the denotational semantics is computable.

Postscript of full publication (346 kilobytes)
(need help viewing Postscript files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.