We present the first algorithm for query learning of a general class of Mealy
machines with timers (MMTs) in a black-box context. Our algorithm is an
extension of the L# algorithm of Vaandrager et al. to a timed setting. Like the
algorithm for learning timed automata proposed by Waga, our algorithm is
inspired by ideas of Maler & Pnueli. Based on the elementary languages of, both
Waga's and our algorithm use symbolic queries, which are then implemented using
finitely many concrete queries. However, whereas Waga needs exponentially many
concrete queries to implement a single symbolic query, we only need a
polynomial number. This is because in order to learn a timed automaton, a
learner needs to determine the exact guard and reset for each transition (out
of exponentially many possibilities), whereas for learning an MMT a learner
only needs to figure out which of the preceding transitions caused a timeout.
As shown in our previous work, this can be done efficiently for a subclass of
MMTs that are race-avoiding: if a timeout is caused by a preceding input then a
slight change in the timing of this input will induce a corresponding change in
the timing of the timeout ("wiggling"). Experiments with a prototype
implementation, written in Rust, show that our algorithm is able to efficiently
learn realistic benchmarks.

我们提出了第一个用于黑盒上下文中的具有计时器的 Mealy 机组的查询学习算法。该算法扩展了 Vaandrager 等人的 L＃算法，以应用于定时设置。通过使用符号查询实现的我们的算法仅需要多项式数量的具体查询，相较于 Waga 的算法的指数数量的具体查询，该算法能有效学习实际基准测试组。