Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Myhill-Nerode style Characterization for Timed Automata With Integer Resets

Kyveli Doveri, Pierre Ganty, B. Srivathsan

TL;DR

This work develops an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form and shows that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K.

Abstract

The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages. In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form.

A Myhill-Nerode style Characterization for Timed Automata With Integer Resets

TL;DR

This work develops an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form and shows that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K.

Abstract

The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages. In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form.
Paper Structure (5 sections, 3 theorems, 5 equations, 3 figures)

This paper contains 5 sections, 3 theorems, 5 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Languages with Integer Resets
  4. Strict 1-IRTA
  5. From Equivalences to Automata and Back

Key Result

Theorem 1

Let $L$ be a language of finite words.

Figures (3)

  • Figure 1: Automaton accepting $L=\{ (t_1\cdot a)\ldots (t_n\cdot a) \mid t_1+\dots +t_n=1\}$ with alphabet $\Sigma=\{a\}$.
  • Figure 2: Automaton accepting $L_2 = \{(t_1 \cdot a) (t_2 \cdot b) \mid \text{either } 0 < t_1 < 1 \text{ and } t_1 + t_2 = 1, \text{ or } 1 < t_1 < 2 \text{ and } t_1 + t_2 = 2 \}$ with alphabet $\Sigma=\{a,b\}$
  • Figure 3: A strict $1$-IRTA with alphabet $\Sigma=\{a\}$ accepting $M=\{u \in \mathbb{T}\Sigma^{*}\mid \mathit{c}^{1}(u)=0\}$.

Theorems & Definitions (8)

  • Theorem 1: Myhill-Nerode theorem
  • Theorem 2
  • Example 3
  • Definition 4
  • Example 5
  • Example 6
  • Proposition 6: see also Theorem 1 bhaveAddingDenseTimedStack2017
  • Definition 7: $L$-preserving, $K$-monotonic