Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Greybox Learning of Languages Recognizable by Event-Recording Automata

Anirban Majumdar, Sayan Mukherjee, Jean-François Raskin

TL;DR

This work introduces a greybox learning framework for ERA-definable timed languages that learns a minimal-state DERA by leveraging fixed region-semantics rather than learning the region automaton itself. By formulating RW_K(L) and exploiting RegL(Σ,K) as a known constraint, the method couples an L*-style learning process with semantic inclusion queries to obtain compact DERAs that exactly recognize the target language. The tLSep algorithm combines a strongly-complete 3DFA learner with a heuristic that derives a small consistent automaton Ci, ensuring correctness via inclusion checks and counterexamples, and achieving minimality in practice. Empirical results and discussions indicate improved explainability and efficiency over prior approaches, with potential extensions to zones and broader timed-language classes.

Abstract

In this paper, we revisit the active learning of timed languages recognizable by event-recording automata. Our framework employs a method known as greybox learning, which enables the learning of event-recording automata with a minimal number of control states. This approach avoids learning the region automaton associated with the language, contrasting with existing methods. We have implemented our greybox learning algorithm with various heuristics to maintain low computational complexity. The efficacy of our approach is demonstrated through several examples.

Greybox Learning of Languages Recognizable by Event-Recording Automata

TL;DR

This work introduces a greybox learning framework for ERA-definable timed languages that learns a minimal-state DERA by leveraging fixed region-semantics rather than learning the region automaton itself. By formulating RW_K(L) and exploiting RegL(Σ,K) as a known constraint, the method couples an L*-style learning process with semantic inclusion queries to obtain compact DERAs that exactly recognize the target language. The tLSep algorithm combines a strongly-complete 3DFA learner with a heuristic that derives a small consistent automaton Ci, ensuring correctness via inclusion checks and counterexamples, and achieving minimality in practice. Empirical results and discussions indicate improved explainability and efficiency over prior approaches, with potential extensions to zones and broader timed-language classes.

Abstract

In this paper, we revisit the active learning of timed languages recognizable by event-recording automata. Our framework employs a method known as greybox learning, which enables the learning of event-recording automata with a minimal number of control states. This approach avoids learning the region automaton associated with the language, contrasting with existing methods. We have implemented our greybox learning algorithm with various heuristics to maintain low computational complexity. The efficacy of our approach is demonstrated through several examples.
Paper Structure (14 sections, 16 theorems, 2 equations, 7 figures, 2 tables)

This paper contains 14 sections, 16 theorems, 2 equations, 7 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries and notations
  3. greybox learning framework
  4. The learning protocol
  5. The region language associated to a timed language
  6. (Strongly-)complete 3DFAs
  7. The tLSep algorithm
  8. Learning the 3DFA $D_i$
  9. Checking if the 3DFA $D_i$ is (strongly-)complete
  10. Computing a small candidate $C_i$ from $D_i$
  11. Checking if $C_i$ is a solution
  12. Correctness of the tLSep algorithm
  13. Implementation and its performance
  14. Discussions

Key Result

Lemma 2

For every $K$-ERA $A$, there exists a $K$-DERA $A'$ such that $L^{\mathsf{tw}}(A) = L^{\mathsf{tw}}(A')$ and there exists a $K$-DERA $\overline{A'}$ such that $\overline{L^{\mathsf{tw}}(A)} = L^{\mathsf{tw}}(\overline{A'})$.

Figures (7)

  • Figure 1: A DERA that accepts timed words where every $a$ is followed by a $b$ after exactly $1$ time unit and every $b$ is followed by an $a$ within $1$ time units
  • Figure 2: Illustration of the two completeness criteria
  • Figure 3: Overview of the tLSep algorithm
  • Figure 4: Overview of the tLSep algorithm with heuristics
  • Figure 5: Explainability of tLSep
  • ...and 2 more figures

Theorems & Definitions (24)

  • Definition 1: ERA
  • Lemma 2: AFH99
  • Example 3
  • Lemma 4
  • Lemma 5
  • Example 6
  • Remark 7
  • Lemma 8
  • Definition 9: The region language
  • Lemma 10
  • ...and 14 more