Model-based testing (MBT) derives test suites from a behavioural specification of the system under test. In practice, engineers favour simple models, such as labelled transition systems (LTSs). However, to deal with quiescence - the absence of observable output - in practice, a time-out needs to be set to conclude observation of quiescence. Timed MBT exists, but it typically relies on the full arsenal of timed automata (TA).

We present a lifting operator X that adds timing without the TA overhead: given an, X introduces a single clock for a user chosen time bound $M>0$ to declare quiescence. In the timed automaton, the clock is used to model that outputs should happen before the clock reaches value $M$, while quiescence occurs exactly at time M. This way we provide a formal basis for the industrial practice of choosing a time-out to conclude quiescence. Our contributions are threefold: (1) if an implementation conforms under ioco, its lifted version conforms under timed tiocoM, (2) applying X before or after the standard ioco test-generation algorithm yields the same set of tests, and (3) the lifted TA test suite and the original LTS test suite deliver identical verdicts for every implementation.