Learning Deterministic Automata On Infinite Words

We study active learning of deterministic infinite-words automata. In our framework, the teacher answers not only membership and equivalence queries, but also provides the loop index of the target automaton on wv(omega), which is the minimal number of letters of wv(omega) past which the target automaton reaches the final cycle on wv(omega). We argue that in potential applications if one can answer Boolean part in membership (and equivalence) queries, one can compute the loop index as well.Our framework is similar to the one of Angluin's L*-algorithm, but the crucial difference is that the queries about the loop index depend on a particular automaton representing an omega-regular language. This allows us to bypass the NP-hardness coming from the minimisation problem for deterministic Buchi automata and provide a polynomial-time algorithm for learning deterministic Buchi automata. We adapt this algorithm to deterministic infinite-word weighted automata with LIMINF and LIMSUP value functions, which, treated as parity automata, can recognize all omega-regular languages.