Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Detailed Account of Compositional Automata Learning through Alphabet Refinement

Leo Henry, Thomas Neele, Mohammad Reza Mousavi, Matteo Sammartino

Abstract

Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches have recently emerged to address scalability to concurrent systems. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets, characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We extend $L^{\star}$ to handle partial and potentially spurious information arising when learning components from global observations only. We establish correctness and termination of the full algorithm. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments on more than 630 subject systems show that CoalA delivers up to five orders of magnitude fewer membership queries than monolithic learning, and achieves better scalability in equivalence queries on systems with significant concurrency.

A Detailed Account of Compositional Automata Learning through Alphabet Refinement

Abstract

Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches have recently emerged to address scalability to concurrent systems. We take a significant step beyond available results, including those by the authors, and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. Our approach automatically refines the global alphabet into component alphabets while learning the component models. We develop a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets, characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. We extend to handle partial and potentially spurious information arising when learning components from global observations only. We establish correctness and termination of the full algorithm. We provide an implementation, called CoalA, using the state-of-the-art active learning library LearnLib. Our experiments on more than 630 subject systems show that CoalA delivers up to five orders of magnitude fewer membership queries than monolithic learning, and achieves better scalability in equivalence queries on systems with significant concurrency.

Paper Structure

This paper contains 33 sections, 18 theorems, 15 equations, 10 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Notation and terminology.
  5. Labeled Transition Systems and their Languages
  6. Active Automata Learning
  7. $\mathtt{L^*}$ algorithm
  8. Foundation and Overview of the Approach
  9. Observations and Distributions.
  10. Overview of the Approach
  11. Local Learners and The Adapter
  12. The Orchestrator
  13. Local Learners and The Adapter
  14. Query Adapter
  15. Membership Queries
  16. ...and 18 more sections

Key Result

Lemma 3.5

Given $n$ LTSs $T_i = (S_i, \Sigma_i, \to_i, \hat{s}\xspace_i)$ for $1 \leq i \leq n$ and their parallel composition $\mathop{{\hbox{$\parallel$}}}_{i=1}^n T_i$, for any word $\sigma\in(\bigcup_{i=1}^n \Sigma_i)^{*}$, $(\hat{s}\xspace_1, \dots, \hat{s}\xspace_n)\mathrel{{\raisebox{-1pt}{$\xrightarro

Figures (10)

  • Figure 1: The parallel composition of two LTSs.
  • Figure 2: Active automata learning for a target language $\mathcal{L}$.
  • Figure 3: A closed and consistent observation table and the LTS that can be constructed from it.
  • Figure 4: Architecture for the compositional learning algorithm. The Orchestrator instantiates the Adapter and Learners according to the current distribution $\Omega$. It can observe queries posed by the Adapter as well as the Teacher's answer.
  • Figure 5: Running example consisting of two LTSs $T_1$ and $T_2$, their parallel composition $T$.
  • ...and 5 more figures

Theorems & Definitions (74)

  • Definition 3.1: Labeled Transition System
  • Definition 3.2: Language of an LTS
  • Remark 3.3
  • Definition 3.4: Parallel composition
  • Lemma 3.5
  • proof
  • Definition 3.6: Parallel composition of languages
  • Lemma 3.7
  • proof
  • Example 3.8: Running example
  • ...and 64 more