Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Evgenii Vinarskii, Jakub Ruszil, Adam Roman, Natalia Kushik

TL;DR

The paper addresses the problem of final state identification in Timed Finite State Machines with output delays by formalizing homing and synchronizing sequences for this timed setting. It develops two key approaches: a truncated successor tree method to derive shortest HS/SS for weakly-complete TFSMs, and a region FSM abstraction that preserves essential behavior while enabling untimed analysis. The results establish that existence checks for HS/SS are polynomial, while deriving the shortest sequences is NP-hard, and provide bounds on sequence lengths via region-based reductions. The work further analyzes TFSMs with point intervals, showing limitations of region-based methods for homing, and introduces timed output tails and an adjusted automaton to obtain HS in this setting, with PSPACE-completeness results in certain cases. Overall, the paper clarifies when untimed abstractions suffice for HS/SS tasks and outlines directions for extending these techniques to more general timed guards and partial observability, with implications for real-time system testing and verification.

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.

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

TL;DR

The paper addresses the problem of final state identification in Timed Finite State Machines with output delays by formalizing homing and synchronizing sequences for this timed setting. It develops two key approaches: a truncated successor tree method to derive shortest HS/SS for weakly-complete TFSMs, and a region FSM abstraction that preserves essential behavior while enabling untimed analysis. The results establish that existence checks for HS/SS are polynomial, while deriving the shortest sequences is NP-hard, and provide bounds on sequence lengths via region-based reductions. The work further analyzes TFSMs with point intervals, showing limitations of region-based methods for homing, and introduces timed output tails and an adjusted automaton to obtain HS in this setting, with PSPACE-completeness results in certain cases. Overall, the paper clarifies when untimed abstractions suffice for HS/SS tasks and outlines directions for extending these techniques to more general timed guards and partial observability, with implications for real-time system testing and verification.

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.

Paper Structure

This paper contains 12 sections, 17 theorems, 7 equations, 15 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Finite State Machines, homing and synchronizing sequences
  4. Timed FSMs with output delays & related notions
  5. Homing and synchronizing sequences for TFSMs with output delays
  6. Final state identification sequences and their properties
  7. Deriving a shortest SS/HS for a TFSM: truncated successor tree approach
  8. Region FSM & its properties
  9. Derivation of the region FSM
  10. Properties of the region FSM for a TFSM with point intervals
  11. Conclusion & future work
  12. Statement proofs for the Reviewers

Key Result

Proposition 1

If $\mathcal{S}$ is a deterministic TFSM with output delays, $s$ is a state of $\mathcal{S}$ and $\alpha \in Dom_{\mathcal{S}}(s)$, then $|next\_state_{\mathcal{S}}(s, \alpha)| = 1$.

Figures (15)

  • Figure 1: FSM $\mathcal{M}_1$
  • Figure 2: TFSM $\mathcal{S}_1$
  • Figure 3: TFSM $\mathcal{S}_2$
  • Figure 4: Fragment of the TST for $\mathcal{S}_2$
  • Figure 5: TFSM $\mathcal{S}_3$
  • ...and 10 more figures

Theorems & Definitions (44)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Proposition 1
  • Definition 5
  • Definition 6
  • Definition 7
  • Lemma 1
  • proof
  • ...and 34 more