DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2024.21

A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets

Authors: Kyveli Doveri, Pierre Ganty, and B. Srivathsan

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

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.

Cite as

Kyveli Doveri, Pierre Ganty, and B. Srivathsan. A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{doveri_et_al:LIPIcs.FSTTCS.2024.21,
  author =	{Doveri, Kyveli and Ganty, Pierre and Srivathsan, B.},
  title =	{{A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.21},
  URN =		{urn:nbn:de:0030-drops-222108},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.21},
  annote =	{Keywords: Timed languages, Timed automata, Canonical representation, Myhill-Nerode equivalence, Integer reset}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.3

Inclusion Testing of Büchi Automata Based on Well-Quasiorders

Authors: Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

We introduce an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramsey-based methods and relies on a least fixpoint characterization of ω-languages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of well-quasiorders on finite words. BAInc is quite simple: it consists of two least fixpoint computations (one for prefixes and the other for periods) manipulating finite sets (of pairs) of states compared by set inclusion, so that language inclusion holds when the sets (of pairs) of states of the fixpoints satisfy some basic conditions. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. We gathered, in addition to existing benchmarks, a large number of new case studies stemming from program verification and word combinatorics, thereby significantly expanding both the scope and size of the available benchmark set. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks. Finally, we demonstrate the generality of our algorithmic framework by instantiating it to the inclusion problem of Büchi pushdown automata into Büchi automata.

Cite as

Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato. Inclusion Testing of Büchi Automata Based on Well-Quasiorders. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doveri_et_al:LIPIcs.CONCUR.2021.3,
  author =	{Doveri, Kyveli and Ganty, Pierre and Parolini, Francesco and Ranzato, Francesco},
  title =	{{Inclusion Testing of B\"{u}chi Automata Based on Well-Quasiorders}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{3:1--3:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.3},
  URN =		{urn:nbn:de:0030-drops-143802},
  doi =		{10.4230/LIPIcs.CONCUR.2021.3},
  annote =	{Keywords: B\"{u}chi (Pushdown) Automata, \omega-Language Inclusion, Well-quasiorders}
}

Search Results

Documents authored by Doveri, Kyveli

A Myhill-Nerode Style Characterization for Timed Automata with Integer Resets

Abstract

Cite as

Inclusion Testing of Büchi Automata Based on Well-Quasiorders

Abstract

Cite as

Thanks for your feedback!

Could not send message