RUS  ENG
Full version
JOURNALS // Modelirovanie i Analiz Informatsionnykh Sistem // Archive

Model. Anal. Inform. Sist., 2020 Volume 27, Number 4, Pages 376–395 (Mi mais723)

This article is cited in 1 paper

Theory of computing

Deriving homing sequences for finite state machines with timed guards

A. S. Tvardovskiia, N. V. Yevtushenkobc

a National Research Tomsk State University, 36 Lenin Ave, Tomsk 634050, Russia
b Ivannikov Institute for System Programming of the RAS, 25 Alexander Solzhenitsyn St., Moscow 109004, Russia
c National Research University Higher School of Economics, 20 Myasnitskaya St., Moscow 101000, Russia

Abstract: State identification is the well-known problem in the theory of Finite State Machines (FSM) where homing sequences (HS) are used for the identification of a current FSM state, and this fact is widely used in the area of software and hardware testing and verification. For various kinds of FSMs, such as partial, complete, deterministic, non-deterministic, there exist sufficient and necessary conditions for the existence ofpreset and adaptive HS and algorithms for their derivation. Nowadays timed aspects become very important for hardware and software systems and for this reason classical FSMs are extended by clock variables. In this work, we address the problem of checking the existence and derivation of homing sequences for FSMs with timed guards and show that the length estimation for timed homing sequence coincides with that for untimed FSM. The investigation is based on the FSM abstraction of a Timed FSM, i.e. on a classical FSM which describes behavior of corresponding TFSM and inherits some of its properties. When solving state identification problems for timed FSMs, the existing FSM abstraction is properly optimized.

Keywords: Finite State Machine, timed guards, FSM abstraction, homing sequence.

UDC: 519.7

MSC: 68Q45

Received: 09.11.2020
Revised: 30.11.2020
Accepted: 16.12.2020

DOI: 10.18255/1818-1015-2020-4-376-395



© Steklov Math. Inst. of RAS, 2024