Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Minimal History-Deterministic Co-Buchi Automata: Congruences and Passive Learning

Christof Löding, Igor Walukiewicz

TL;DR

This work gives a congruence-based description of minimal history-deterministic co-Büchi automata by focusing on pointed pairs and a refined equivalence $ oughapprox_L$. It introduces canonical automata $ ext{A}_{ oughequiv_L}$ whose states are pointed $ oughequiv_L$-classes, and shows how to construct them via safe-SCCs and component automata $C(u,v)$. Building on this, the authors develop a polynomial-time passive learner that infers the minimal automaton from polynomial-sized characteristic data, leveraging the new equivalence $ oughapprox_L$ and a modular component-based learning algorithm. The results provide the first efficient passive learning framework for a non-prefix-independent ω-language class and yield a deeper structural understanding of HD co-Büchi automata with potential impact on synthesis and verification where canonical and learnable representations are valuable. The work also outlines future directions, including extension beyond co-Büchi and development of active learning analogues. All mathematical constructs are expressed within a rigorous congruence-based framework, and the claims are supported by self-contained proofs and complexity analyses $($polynomial in the sample size$)$.

Abstract

Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-Büchi automata, building on the results of Kuperberg and Skrzypczak (2015). We give a congruence-based description of these minimal automata, and a self-contained proof of its correctness. We use this description based on congruences to create a passive learning algorithm that can learn minimal history-deterministic co-Büchi automata from a set of labeled example words. The algorithm runs in polynomial time on a given set of examples, and there is a characteristic set of examples of polynomial size for each minimal history-deterministic co-Büchi automaton.

Minimal History-Deterministic Co-Buchi Automata: Congruences and Passive Learning

TL;DR

This work gives a congruence-based description of minimal history-deterministic co-Büchi automata by focusing on pointed pairs and a refined equivalence . It introduces canonical automata whose states are pointed -classes, and shows how to construct them via safe-SCCs and component automata . Building on this, the authors develop a polynomial-time passive learner that infers the minimal automaton from polynomial-sized characteristic data, leveraging the new equivalence and a modular component-based learning algorithm. The results provide the first efficient passive learning framework for a non-prefix-independent ω-language class and yield a deeper structural understanding of HD co-Büchi automata with potential impact on synthesis and verification where canonical and learnable representations are valuable. The work also outlines future directions, including extension beyond co-Büchi and development of active learning analogues. All mathematical constructs are expressed within a rigorous congruence-based framework, and the claims are supported by self-contained proofs and complexity analyses polynomial in the sample size.

Abstract

Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-Büchi automata, building on the results of Kuperberg and Skrzypczak (2015). We give a congruence-based description of these minimal automata, and a self-contained proof of its correctness. We use this description based on congruences to create a passive learning algorithm that can learn minimal history-deterministic co-Büchi automata from a set of labeled example words. The algorithm runs in polynomial time on a given set of examples, and there is a characteristic set of examples of polynomial size for each minimal history-deterministic co-Büchi automaton.

Paper Structure

This paper contains 20 sections, 46 theorems, 17 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Canonical Automaton
  5. Passive Learning
  6. Overview and Challenges
  7. Equivalence $\mathbin{"\approx_{L}"}$
  8. Components $C(u,v)$ and automaton $\mathcal{A}[\mathcal{C}]$
  9. Idealized learning algorithm
  10. Finding a new pointed element
  11. Passive learning algorithm
  12. Conclusion
  13. Details on Example \ref{['ex:long-SCC-path']}
  14. Proofs from Section \ref{['sec:automaton']}
  15. Proofs from Section \ref{['sec:learning']}
  16. ...and 5 more sections

Key Result

Lemma 1

Every "history-deterministic" co-Büchi automaton can be made "normalized", "semantically-deterministic", and "unsafe-saturated" without changing the language, by respectively modifying the rank of some transitions, removing some states, and adding some $1$-transitions.

Figures (2)

  • Figure 1: Relations $\mathbin{"\sim_L"}$ and $\mathbin{"\equiv_L"}$ for the language of all words over $\{a,b,c\}$ that start with $a$ and have finitely many $c$ or a finite and odd number of $b$, see Examples \ref{['ex:a-start']}, \ref{['ex:a-start-aut']}.
  • Figure 2: The $2$-transitions of the minimal "history-deterministic" co-Büchi automaton for the language from Example \ref{['ex:long-SCC-path']} with state set $Q_k$.

Theorems & Definitions (87)

  • Lemma 1
  • Lemma 2
  • proof
  • Definition 3
  • Lemma 3
  • proof
  • Lemma 4
  • proof
  • Definition 5
  • Theorem 6
  • ...and 77 more