Active Learning of Mealy Machines with Timers
This work addresses a domain-specific problem for researchers in formal methods and timed systems, representing an incremental extension of existing algorithms.
The authors tackled the problem of query learning Mealy machines with timers in a black-box context by presenting the first algorithm for this task, which efficiently learned realistic benchmarks in experiments.
We present the first algorithm for query learning 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 realized using finitely many concrete queries. Experiments with a prototype implementation show that our algorithm is able to efficiently learn realistic benchmarks.