A denotational semantics is presented for ET-LOTOS [LeL94] in the style of semantics for timed CSP, in terms of timed failures with additional information about internal events. This semantics is consistent with the original operational semantics, and is shown to be the weakest congruence stronger than trace equivalence---the weakest useful congruence. 1 Introduction The LOTOS specification language was developed to support specification and design of distributed and communicating systems. Recently, a number of proposals have arisen for incorporating time into the language [LeL94, QFA93, BLT94], enabling the modelling of quantitative timing behaviour. A LOTOS specification consists primarily of a description of desirable behaviour. But we also require a notion of how closely any proposed implementation should resemble that ideal. Many approaches require that an implementation should be at least weakly bisimilar to the specification process. Bisimulation equivalence has the pleasing pr...