Deriving homing sequences for Finite State Machines with timeouts.

The article focuses on the homing problem for Finite State Machines with timeouts (TFSMs), which extends classical FSMs by incorporating clock variables and timeout transitions allowing spontaneous state changes without input. It introduces the notion of a timed homing sequence (HS) for TFSMs, defined as a timed input sequence that drives the system from any initial timed state to a known stable state where it can remain indefinitely waiting for input. The authors propose methods for checking the existence of such HS and deriving them by leveraging FSM abstractions of TFSMs, transforming the timed problem into a classical FSM homing problem with a subset of final states corresponding to stable states. They also discuss the FSM projection approach, which removes timeout transitions to simplify HS derivation, and provide complexity bounds and conditions under which HS exist. The work highlights that, unlike classical FSMs, an HS for a TFSM can be empty if the system naturally stabilizes over time, and suggests future research directions including adaptive HS and extensions to FSMs with timed guards and output timeouts.