In order to understand and verify complex systems, we need accurate models that are either understandable for humans or can be analyzed fully automatically. Such models, however, are typically not available for legacy software. Active automata learning is a black-box technique for constructing state machine models of software and hardware components from information obtained through testing (i.e., providing inputs and observing the resulting outputs) and may thus fill this gap. In many applications, timing plays a crucial role, which in turn makes extending automata learning to a setting that incorporates quantitative timing information challenging. In this talk, we present an active learning algorithm for a general class of Mealy machines with timers (MMTs) in a black-box context. A Mealy machine is a finite state machine that outputs a sequence of symbols for every processed input word. We then augment it with timers that force certain transitions to occur after a certain amount of time has elapsed. Our algorithm is an extension of the L# algorithm of Vaandrager et al. [1] to a timed setting. Like the algorithm for learning timed automata proposed by Waga [2], our algorithm is inspired by ideas of Maler & Pnueli [3]. Based on the elementary languages of [3], 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 a previous work [4], 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.
[1]: Frits W. Vaandrager, Bharat Garhewal, Jurriaan Rot, and Thorsten Wißmann. A new approach for active automata learning based on apartness. TACAS 2022.
[2]: Masaki Waga. Active learning of deterministic timed automata with myhill-nerode style characterization. CAV 2023.
[3]: Oded Maler and Amir Pnueli. On recognizable timed languages. FOSSACS 2004.
[4]: Véronique Bruyère, Guillermo A. Pérez, Gaëtan Staquet, and Frits W. Vaandrager. Automata with timers. FORMATS 2023.