Active Learning of Mealy Machines with Timers

TL;DR

This paper introduces a novel algorithm for actively learning Mealy machines with timers in a black-box setting, extending existing algorithms to handle timing constraints using symbolic queries, and demonstrates its efficiency through experiments.

Contribution

It extends the L# algorithm to timed settings with symbolic queries, enabling efficient learning of timed Mealy machines in black-box scenarios.

Findings

Efficient learning of timed Mealy machines demonstrated on benchmarks.

Symbolic queries enable reasoning on untimed executions.

Prototype implementation shows practical effectiveness.

Abstract

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.