Learning Event-recording Automata Passively

TL;DR

This paper introduces LEAP, a passive learning algorithm for timed languages using event-recording automata, employing state merging and SMT solving to handle sample consistency and automaton inference.

Contribution

The paper presents a novel passive learning algorithm for ERA that combines state merging with SMT-based techniques to handle NP-complete merging decisions.

Findings

Effective in learning ERA from positive and negative samples

Handles NP-complete merging problem with SMT solvers

Can infer any ERA-definable language with appropriate samples

Abstract

This paper presents a state-merging algorithm for learning timed languages definable by Event-Recording Automata (ERA) using positive and negative samples in the form of symbolic timed words. Our algorithm, LEAP (Learning Event-recording Automata Passively), constructs a possibly nondeterministic ERA from such samples based on merging techniques. We prove that determining whether two ERA states can be merged while preserving sample consistency is an NP-complete problem, and address this with a practical SMT-based solution. Our implementation demonstrates the algorithm's effectiveness through examples. We also show that every ERA-definable language can be inferred using our algorithm with a suitable sample.