Abstract:
Finite State Machines (FSMs) are widely used for analysis and synthesis of components of control systems. In order to take into account time aspects, timed FSMs are considered. As the complexity of many problems of analysis and synthesis of digital and hybrid systems including high-quality test derivation significantly depends on the size of the system (component) specification, in this paper, we address the problem of minimizing a FSM with timed guards and input and output timeouts (TFSM). The behavior of a TFSM can be described using a corresponding FSM abstraction and a proposed approach for minimizing a TFSM is based on such abstraction. We minimize not only the number of states as it is done for classical FSMs but also the number of timed guards and timeout duration. We show that for a complete deterministic TFSM there exists the unique minimal (canonical) form, i.e., a unique time and state reduced TFSM that has the same behavior as the given TFSM; for example, this minimal form can be used when deriving tests for checking whether an implementation under test satisfies functional and nonfunctional requirements. A proposed approach for minimizing timed machines can be applied to particular cases of TFSM, i.e. for FSM with timeouts and FSM with timed guards.
Keywords:Timed Finite State Machines, reduced form, minimal form.