A Myhill-Nerode style Characterization for Timed Automata With Integer Resets
<|reference_start|>A Myhill-Nerode style Characterization for Timed Automata With Integer Resets: 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.<|reference_end|>
@article{doveri2024a,
    title={A Myhill-Nerode style Characterization for Timed Automata With Integer
  Resets},
    author={Kyveli Doveri, Pierre Ganty, B. Srivathsan},
    journal={arXiv preprint arXiv:2410.02464},
    year={2024},
    archivePrefix={arXiv},
    eprint={2410.02464},
    primaryClass={cs.FL}
}