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 χ M\! that augments LTSs with time without the overhead of general TA. Given an LTS and a user-defined timeout M>0 , χ M\! 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: ioco coincides with timed tiocoM after lifting, even in the presence of internal (“ τ ”) transitions; (2) We show that χ M\! 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 χ M\! as M -urgent, and ensure our construction is robust under action hiding.