Deriving Homing Sequences for Finite State Machines with Timed Guards
Aleksandr Tvardovskii, Nina Vladimirovna Yevtushenko · Automatic Control and Computer Sciences · 2021
State identification is a well-known problem in the theory of finite state machines (FSM). In this theory homing sequences (HS) allow to identify the current state of an FSM and are widely used for testing and verification of hardware and software systems. Sufficient and necessary conditions for the existence of preset and adaptive HS are established for various kinds of FSMs, such as partial and complete machines, deterministic and nondeterministic, and algorithms for deriving these sequences are proposed when such a sequence exists. Nowadays, time-related aspects must be considered when verifying and testing hardware and software, which is why FSM models are extended by clock variables. This work studies the problems of checking the existence and synthesis of preset and adaptive homing sequences for FSMs with timed guards and we show that the length estimates for these sequences coincide with the estimates for classical FSMs. A proposed approach is based on the FSM abstraction of a timed FSM, that is, on the description of this timed FSM by a corresponding FSM that preserves the properties of the timed FSM related to homing sequences.