UTFacultiesEEMCSEvidence-Driven Black-Box CheckingProject News"Active Learning of Mealy Machines with Timers" accepted at QEST+FORMATS

"Active Learning of Mealy Machines with Timers" accepted at QEST+FORMATS

The paper Active Learning of Mealy Machines with Timers by Véronique Bruyère, Bharat Garhewal, Guillermo Perez, Gaëtan Staquet and Frits Vaandrager has been accepted for publication at QEST+FORMATS 2025.

Abstract: We present the first algorithm for query learning of a class of Mealy machines with timers in a black-box context. Our algorithm is an extension of the L# algorithm of Vaandrager et al. to a timed setting. We rely on symbolic queries which empower us to reason on untimed executions while learning. Similarly to the algorithm for learning timed automata of Waga, these symbolic queries can be implemented using finitely many concrete queries. Experiments with a prototype implementation show that our algorithm is able to efficiently learn realistic benchmarks. 

Published on June 13th, 2025