modular design and development of automata learning algorithms, with correctness-by-construction guarantees


Learning Nominal Automata (extended version of POPL'17 talk)
Automata learning, or regular inference, is a widely used technique for creating an automaton model from observations. In recent years, it has been successfully applied to the verification of security protocols, hardware, and software systems. The original algorithm L* works for deterministic finite automata, and is only capable of learning control-flow models. In this talk I will present an extension of L* to learn combined control/data-flow models in the form of nominal automata, which are acceptors of languages over infinite (structured) alphabets. After recalling L*, I will briefly present the theory of nominal sets. Then I will show how this theory enables extending L* to infinite alphabets in a seamless way, with almost no modifications to the original code. Finally, I will give a short demo of a tool based on this work, currently being developed at UCL.
Matteo Sammartino
RISE seminar cycle, IST Austria
CALF: Categorical Automata Learning Framework
Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there was no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs. In the first part of this talk, I recall the details of active learning algorithms for DFAs. The second part then introduces our category-theoretic formalism that provides an appropriately abstract foundation for studying automata learning. I will also discuss formal relations between algorithms for learning, testing, and minimisation within our framework.
Gerco van Heerdt
PPLV seminar cycle, UCL