Inferring Symbolic Automata

TL;DR

This work analyzes the learnability of symbolic finite state automata (SFAs) under two paradigms: query learning (L*-style) and identification in the limit with polynomial time/data. It first derives a necessary condition for efficient query-learning of SFAs and provides the first negative result for SFAs over the propositional Boolean algebra, highlighting limits of L*-style approaches. Focusing on identification in the limit, it introduces generalize, concretize, and decontaminate as key tools and proves a sufficient condition for efficient identifiability, showing that SFAs over monotonic algebras are efficiently identifiable, while those over propositional algebras are not unless $P=NP$. The paper also analyzes automata procedures with a triple size measure $(n,m,l)$ and explores transformations to Neat/Normalized/Feasible forms, revealing that neat and monotonic settings yield favorable complexity. Overall, the results clarify when SFAs can be learned efficiently in verification settings and lay groundwork for broader exploration of characteristic samples and learnability across automata models.

Abstract

We study the learnability of symbolic finite state automata (SFA), a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all obtained results are positive. We provide a necessary condition for efficient learnability of SFAs in this paradigm, from which we obtain the first negative result. The main focus of our work lies in the learnability of SFAs under the paradigm of identification in the limit using polynomial time and data, and its strengthening efficient identifiability, which are concerned with the existence of a systematic set of characteristic samples from which a learner can correctly infer the target language. We provide a necessary condition for identification of SFAs in the limit using polynomial time and data, and a sufficient condition for efficient learnability of SFAs. From these conditions we derive a positive and a negative result. The performance of a learning algorithm is typically bounded as a function of the size of the representation of the target language. Since SFAs, in general, do not have a canonical form, and there are trade-offs between the complexity of the predicates on the transitions and the number of transitions, we start by defining size measures for SFAs. We revisit the complexity of procedures on SFAs and analyze them according to these measures, paying attention to the special forms of SFAs: normalized SFAs and neat SFAs, as well as to SFAs over a monotonic effective Boolean algebra. This is an extended version of the paper with the same title published in CSL'22.

Figures (9)

• Figure 1: The SFA $\mathcal{M}$ over ${\mathpzc{A_\mathbb{N}}}$
• Figure 1: ${\textsf{Concretize}}_{{\mathbb{M}}_\mathpzc{A}}(\mathcal{M})$
• Figure 2: A schematic description of algorithms ${{\textbf{CharSFA}}}$ and ${{\textbf{InferSFA}}}$
• Figure 3: Visualisation of Example \ref{['exa:genIntervals']}
• Figure 3: ${\textsf{Decontaminate}}_{{\mathbb{M}}_{\mathpzc{A_m}}}$ -- finding the necessary letters for a characteristic sample

Theorems & Definitions (57)

• Example 2.1
• Example 2.2
• Example 3.1
• Lemma 4.1
• Lemma 4.2
• Lemma 4.3
• proof
• Lemma 5.1
• proof
• Lemma 5.2