Canonical Algebraic Generators in Automata Learning

TL;DR

This paper investigates the existence of canonical minimal automata in automata learning, focusing on subclasses of acceptors where such canonical forms can be identified, which is crucial for verification and modeling.

Contribution

It extends the concept of canonical automata to subclasses of acceptors, identifying conditions under which minimal representatives are unique and can be effectively learned.

Findings

Canonical automata exist for certain subclasses of acceptors.

Non-deterministic automata can be exponentially more succinct than deterministic ones.

Identified subclasses admit canonical size-minimal automata, aiding automata learning and verification.

Abstract

Many methods for the verification of complex computer systems require the existence of a tractable mathematical abstraction of the system, often in the form of an automaton. In reality, however, such a model is hard to come up with, in particular manually. Automata learning is a technique that can automatically infer an automaton model from a system -- by observing its behaviour. The majority of automata learning algorithms is based on the so-called L* algorithm. The acceptor learned by L* has an important property: it is canonical, in the sense that, it is, up to isomorphism, the unique deterministic finite automaton of minimal size accepting a given regular language. Establishing a similar result for other classes of acceptors, often with side-effects, is of great practical importance. Non-deterministic finite automata, for instance, can be exponentially more succinct than deterministic ones, allowing verification to scale. Unfortunately, identifying a canonical size-minimal non-deterministic acceptor of a given regular language is in general not possible: it can happen that a regular language is accepted by two non-isomorphic non-deterministic finite automata of minimal size. In particular, it thus is unclear which one of the automata should be targeted by a learning algorithm. In this thesis, we further explore the issue and identify (sub-)classes of acceptors that admit canonical size-minimal representatives.