Discrete-Time Refinement of Hybrid Automata

Notations like hybrid automata are highly useful in the development process of hybrid systems to document requirements in early design steps. When it comes to implementation a part of the requirements will be realized in software in a discrete-time manner. We therefore study sufficient conditions which ensure that an automaton operating in discrete-time refines a hybrid automaton with its underlying continuous time model. Our notion of refinement provides that vital properties which have been established for the hybrid automaton also hold for its refinement