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

TL;DR

This paper introduces a Nerode-style equivalence for timed automata with integer resets, leading to a canonical automaton and an efficient active learning algorithm with polynomial query complexity.

Contribution

It provides the first Myhill-Nerode theorem for timed automata with integer resets and develops a canonical automaton and learning algorithm based on this equivalence.

Findings

Establishes a Nerode-style equivalence depending on a constant K.

Proves a Myhill-Nerode theorem for this class of timed automata.

Develops an active learning algorithm with polynomial query complexity.

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.