Learning Event-recording Automata Passively

2025/08/05 by Anirban Majumdar, Sayan Mukherjee, Majumdar, Anirban +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Machine Learning and Algorithms #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2508.03627

openalex publication_date 2025/08/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Citations

• Greybox Learning of Languages Recognizable by Event-Recording Automata
• Active Learning of Mealy Machines with Timers
• Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
• LTL Reactive Synthesis with a Few Hints
• Active Learning of One-Clock Timed Automata using Constraint Solving
• A New Approach for Active Automata Learning Based on Apartness
• Active learning of timed automata with unobservable resets
• Timed k-Tail: Automatic Inference of Timed Automata
• A theory of timed automata
• The benefits of relaxing punctuality

Related

• Greybox Learning of Languages Recognizable by Event-Recording Automata
• Active learning of timed automata with unobservable resets
• Extending AALpy with Passive Learning: A Generalized State-Merging Approach
• Scalable Learning of One-Counter Automata via State-Merging Algorithms
• Human in the Loop: Interactive Passive Automata Learning via Evidence-Driven State-Merging Algorithms