2026-07-22T11:56:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22210 2024-12-05T15:18:03Z ddc:004 open_access

A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets Doveri, Kyveli Ganty, Pierre Srivathsan, B. Timed languages Timed automata Canonical representation Myhill-Nerode equivalence Integer reset 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kyveli Doveri and Pierre Ganty and B. Srivathsan 2024 Is Part Of LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2024.21 urn:nbn:de:0030-drops-222108 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.21 eng https://creativecommons.org/licenses/by/4.0/legalcode