Almost ASAP semantics: From timed models to timed implementations

Abstract

In this paper, we introduce a parametric semantics for timed controllers called the Almost ASAP (as soon as possible) semantics. This semantics is a relaxation of the usual ASAP semantics (also called the maximal progress semantics) which is a mathematical idealization that cannot be implemented by any physical device no matter how fast it is. On the contrary, any correct Almost ASAP controller can be implemented by a program on a hardware if this hardware is fast enough. We study the properties of this semantics and show how it can be analyzed using the tool HyTech. © BCS 2005.