Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive Learning

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.

First revision of journal submission from previous version. Fixed some typos and arguments in proofs; added some more explanations in examples. The numbering of lemmas, theorems etc. did not change compared to previous version