In this paper, we introduce a parametric semantics for timed controllers called the Almost ASAP semantics. This semantics is a relaxation of the usual ASAP semantics (also called the maximal progress semantics) which is a mathematical idealization that can not 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, show how it can be analyzed using the tool HyTech, and illustrate its practical use on examples.
展开▼
