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

TL;DR

This paper introduces a congruence-based framework for minimal history-deterministic co-Büchi automata and presents a polynomial-time passive learning algorithm for these automata from labeled examples.

Contribution

It provides a new congruence characterization of minimal history-deterministic co-Büchi automata and a passive learning algorithm with polynomial complexity.

Findings

Congruence-based description of minimal automata

Passive learning algorithm runs in polynomial time

Existence of polynomial-sized characteristic sets

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.