Time for Quiescence: Modelling Quiescent Behaviour in Testing via Time-Outs in Timed Automata

Model-based testing (MBT) derives test suites from a behavioural specification of the system under test. In industrial practice, engineers favor simple models such as labelled transition systems (LTSs). However, handling quiescence (i.e., the absence of observable outputs) requires introducing a time-out to determine when quiescence can be concluded. While timed versions of model-based testing address this, they usually rely on the full expressive power of timed automata (TA), which is often more complex than needed. We introduce a lightweight lifting operator [Formula: see text] that augments LTSs with time without the overhead of general TA. Given an LTS and a user-defined timeout [Formula: see text], [Formula: see text] adds a single clock that restricts observable outputs to occur strictly before M and makes quiescence observable exactly at time M . Our contributions are as follows: (1) We show that lifting preserves input-output conformance: [Formula: see text] coincides with timed [Formula: see text] after lifting, even in the presence of internal ("τ ") transitions; (2) We show that [Formula: see text] commutes with test generation: applying the lifting before or after standard ioco test generation yields the same test suite; (3) We show that lifted and untimed test suites assign identical verdicts to all implementations; (4) We characterise the timed languages induced by [Formula: see text] as M -urgent, and ensure our construction is robust under action hiding.