Pith. Sign in

REVIEW

Minimal History-Deterministic Co-B\"uchi Automata: Congruences and Passive Learning

PaperPDF from arXiv

data files

ReviewThe objections and verdict, as JSON Paper breakdownThe authors' claims, conditions and measurements, as JSON Signed receiptProof this review has not been altered
X Bluesky LinkedIn Reddit Hacker News
Christof Löding, Igor Walukiewicz

Formal Languages and Automata Theory · Submitted 20 May 2025 · 19 references

Pith's reading: The paper gives a congruence-based canonical form for minimal history-deterministic co-Büchi automata and a passive learning algorithm that is polynomial in time and data, the first for a nontrivial prefix-independent class of omega-languages.

T0 · AI review

How this review was made: An AI referee (deepseek-v4-flash) read the paper on August 7, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

  1. T0 AI review An AI read the paper and answered a fixed list of questions.
  2. T1 Audit Automatic checks that the references and files the paper relies on exist and match.
  3. T2 Compute The paper's code or calculations re-run with the same results.
  4. T3 Formal statement The claims written out in a formal math language a computer can read.
  5. T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· Ask about this paper · The compiled record · Read the full review →
Challenge this review Comment (0) Read on arXiv ↗
Cite ▾
arXiv ID2505.14304 (version 5)
Pith IDZQDPED32, Pith's permanent record of this paper and its review
CitationChristof L\"oding, Igor Walukiewicz. "Minimal History-Deterministic Co-B\"uchi Automata: Congruences and Passive Learning." arXiv:2505.14304 (2025). https://pith.science/paper/ZQDPED32
Cite this reviewBibTeX for Pith's review of this paper
Claim paper
The paper

The paper claims

The paper gives a congruence-based canonical form for minimal history-deterministic co-Büchi automata and a passive learning algorithm that is polynomial in time and data, the first for a nontrivial prefix-independent class of omega-languages.

The reading

Automata are simplified machines that read words and decide whether they belong to a language. This paper studies automata that read infinite words and use a co-Büchi acceptance condition: a run is accepted if, after some point, it only takes safe transitions. History-deterministic automata are nondeterministic machines whose choices can be made online, from the prefix read so far, without knowing the future. For this class, minimal automata exist and can be minimized efficiently, but until now there was no structural description of what the minimal automaton looks like.

The authors define a congruence on pairs of finite words: two pairs (u,v) and (u',v') are equivalent if their concatenations belong to the same right-congruence class of the language and they have the same set of safe extensions. Not all equivalence classes become states; only those containing a pointed pair, a pair whose safe language is minimal in a precise sense. The resulting automaton has one state per pointed class, and transitions extend the second component of the pair. This gives a direct, self-contained construction of the minimal automaton.

The same description powers a passive learning algorithm. Given a sample of ultimately periodic words labeled as accepted or rejected, the learner infers the pointed congruence classes, constructs components for each safe strongly connected component, and combines them. The main challenges are that the total number of congruence classes can be exponential, and some classes have only exponentially long representatives. The algorithm uses a helper relation that can be tested from finite samples and a measure based on sets of states reachable by safe transitions to find polynomial-size pointed representatives.

Extended reading notes

Core claim

Theorem 3.10: The automaton A≡L is the minimal history-deterministic co-Büchi automaton for L. Combined with Theorem 4.20: Learn(S) is a consistent polynomial time passive learner that learns A≡L for each co-Büchi language L in the limit from polynomial data. If correct, the congruence-based construction is the canonical form, and the learner is the first efficient passive learner for a class of omega-languages that remains nontrivial on prefix-independent languages.

Load-bearing premise

The polynomial-time and polynomial-data guarantees of Theorem 4.20 depend on Lemma 4.16's bound that every state of A≡L has a central sequence of length at most α^3. The proof of Lemma 4.16 appears to have a gap: when z1 is not central and p_i1 --z1:2--> p_j1, appending the central sequence z_j1 of p_j1 still gives p_i1 --z1 z_j1:2--> p_j1, so the claimed increase in the smallest offending index does not follow. If central sequences can be superpolynomial, Proposition 4.19's polynomial bound on the words produced by FindPointed, and with it the polynomial-data claim, would fail. Similarly, Lemma 4.15's use of safe-determinism to conclude |Ri| ≥ |Ri+1| needs injectivity of the word map, which safe-determinism alone does not provide.

Original abstract

Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-B\"uchi 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\"uchi 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\"uchi automaton.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-09-23: 1 request, 3,704 input tokens.

What the abstract itself states, as probabilities: claims first 0.07 · states limitation 0.12 · human participants 0.02 · controlled comparison 0.02 · randomized assignment 0.01 · states quantitative result 0.81 · compares with prior results 0.74 · mentions code or data availability 0.03.

The abstract, sentence by sentence

arXiv listing abstract v5. Results and the main claim are underlined; .

Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-B\"uchi 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\"uchi 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\"uchi automaton.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#sentencerolethe authors' own workstates the main conclusionstrength
s0 Abu Radi and Kupferman (2019) demonstrated the efficient minimization of history-deterministic (transition-based) co-B\"uchi automata, building on the results of Kuperberg and Skrzypczak (2015). background 1.00 0.03 0.05 asserted 1.00
s1 We give a congruence-based description of these minimal automata, and a self-contained proof of its correctness. contribution 1.00 0.96 0.25 asserted 1.00
s2 We use this description based on congruences to create a passive learning algorithm that can learn minimal history-deterministic co-B\"uchi automata from a set of labeled example words. contribution 0.75 0.95 0.34 asserted 1.00
s3 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\"uchi automaton. result 0.97 0.91 0.29 asserted 1.00

What kind of paper the classifier reports this is: method or tool 0.82 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read
  • arXiv listing abstract v5
not examined
  • full text
  • figures and tables
  • references and citing sentences
  • relations to other papers
levels run
  • P abstract
not run
  • S sections
  • T body sentences
  • C citations
  • R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures
Figure 1. Relations ∼L and ≡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 3.4, 3.9. While the notion pointed is a central definition of the paper, it is not easy to motivate it at this stage. We try to give some intuition in the following example, and give some motivations later when we show technical properties of pointed elements and classes. Example 3.3. Continuing Example 3.1, the pointed pairs are those of the form (u, v) where v contains all but one of the letters. Indeed, if v does not contain ai…
Figure 2. The 2-transitions of the minimal history-deterministic co-B¨uchi automaton for the language from Example 4.9 with state set Qk. Now note that θ(ak) = {q 0 0 , . . . , q0 k−1 , q1 k }, and θ(akvk) = {q 1 0 , . . . , q1 k−1 , q1 k } because (q 0 0 , . . . , q0 k−1 ) vk:2 −−→ (q 1 0 , . . . , q1 k−1 ) as explained above. As every v with θ(v) = {q 1 0 , . . . , q1 k−1 , q1 k } needs to contain ak followed by an x with (q 0 0 , . . . , q0 k−1 ) x:2 −−→ (q 1 0 , . . . , q1 k−1 ), and since vk is the shortest such x, we obtain that akvk is indeed the

Figures reproduced from arXiv:2505.14304 by the authors.

Human review

How Pith checks papers → · Full audit of this paper →

References
How the literature uses it

What this paper does with the arXiv papers it cites

Each citing sentence is taken from the citing paper's LaTeX source and typed by Pith's classifier. A label appears at probability 0.8 or more (0.95 for support), a contest at 0.7 or more; the quoted words are the citing authors'. How each label was checked · JSON

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.