Learning optimisation models of automata
Verification is the domain of computer science aiming at checking and certifying computer systems. Computer systems are used at all levels of society and peoples' lives and it is paramount to verify that they behave the way they are designed to and that we expect (think, e.g., about planes auto-pilot or self-driving cars).
Unfortunately, the verification of complex systems encounters limits: there is no universal fully automated way to verify every system and one needs to find a good trade-off between the constraints of time, memory space and accuracy, which are often difficult to overcome.
The aim of this project is to apply learning techniques in verification to improve the efficiency of algorithms which certify computer systems and to compute fast accurate models for real-life systems.
More precisely, the project will focus on automata. Automata are one of the mathematical tools used in verification to model computer or real-life systems. Giving certifications on these systems often boils down to running some algorithms on the corresponding automata. The efficiency of such algorithms usually depends on the size of the considered automaton. Minimizing automata is thus a paramount problem in verification to verify large computer or real-life systems faster.
Our objective is studying the minimization of some streaming models of quantitative automata using machine learning techniques. More precisely, we are interested in cost register automata over the tropical semiring. These automata are streaming models, in the sense that the input is not stored but received as a stream of data and dealt with on the fly, thus being particularly suitable for the treatment of big data. They are also suited to deal with optimisation problems: minimizing the resource consumption of a system or computing the worst-case running time of a program, for example.
This project aims at adapting the classic Angluin L* algorithm that learns automata and weighted automata, to learn optimisation models of automata.