Studying homing and synchronizing sequences for Timed Finite State Machines with output delays

TL;DR

This paper studies the properties and methods for identifying homing and synchronizing sequences in Timed Finite State Machines with output delays, highlighting differences from untimed models and analyzing computational complexity.

Contribution

It formally defines homing and synchronizing sequences for TFSMs with output delays and evaluates various approaches and their applicability for deriving these sequences.

Findings

Certain properties from untimed FSMs do not hold for TFSMs.

Approaches like tree-based and abstraction-based methods are applicable to specific subclasses.

The complexity of checking existence and deriving shortest sequences is analyzed.

Abstract

The paper introduces final state identification (synchronizing and homing) sequences for Timed Finite State Machines (TFSMs) with output delays and investigates their properties. We formally define the notions of homing sequences (HSs) and synchronizing sequences (SSs) for these TFSMs and demonstrate that several properties that hold for untimed machines do not necessarily apply to timed ones. Furthermore, we explore the applicability of various approaches for deriving SSs and HSs for Timed FSMs with output delays, such as truncated successor tree-based and FSM abstraction-based methods. Correspondingly, we identify the subclasses of TFSMs for which these approaches can be directly applied and those for which other methods are required. Additionally, we evaluate the complexity of existence check and derivation of (shortest) HSs / SSs for TFSMs with output delays.