Abstract:

Timed CSP has a denotational semantics in terms of timed failures. In this talk we investigate how this approach to semantics may be applied to a timed version of LOTOS, while remaining consistent with its operational semantics. It turns out that timed failures alone are not adequate, and that an additional component is required in the semantics in order to deal with operators that are sensitive to internal actions. The resulting denotational semantics is shown to be the weakest congruence stronger than trace equivalence. We also discuss the relationship with other approaches to timed LOTOS.