Gaëtan Staquet

Kévin Dubrulle, Véronique Bruyère, Guillermo A. Pérez et al.

As an alternative to visibly pushdown automata, we introduce visibly recursive automata (VRAs), composed of a set of classical automata that can call each other. VRAs are a strict extension of so-called systems of procedural automata, a model proposed by Frohme and Steffen. We study the complexity of standard language-theoretic operations and classical decision problems for VRAs. Since the class of deterministic VRAs forms a strict subclass in terms of expressiveness, we propose a (weaker) notion that does not restrict expressive power and which we call codeterminism. Codeterminism comes with many desirable algorithmic properties that we demonstrate by using it, e.g., as a stepping stone towards implementing complementation of VRAs.

Véronique Bruyère, Bharat Garhewal, Guillermo A. Pérez et al.

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.