Sciweavers

Share
FOSSACS
2006
Springer

Denotational Semantics of Hybrid Automata

10 years 1 months ago
Denotational Semantics of Hybrid Automata
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.
Abbas Edalat, Dirk Pattinson
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FOSSACS
Authors Abbas Edalat, Dirk Pattinson
Comments (0)
books