[Lrde Annonce] exposé de Maximilien Collenge sur des automates de Büchi avec compteurs le 4 décembre au LRDE

Le 4 décembre, à 14h, au LRDE (https://www.lrde.epita.fr/wiki/Contact), Maximilien Collenge, actuellement en post-doc à l'université de Genève, fera un exposé sur les automates de Büchi avec compteurs. Abstract: Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The automata-based approach expresses the property as an automaton then analyses its synchronisation with the model automaton. This method can be extended with various automata flavors to handle quantitative properties. When the quantitative domain is discrete, quantities can be encoded as automata states, and quantitative model-checking is thus reduced to qualitative model-checking. To this end, the initial model is enhanced with new state variables that keep track of the observed quantities, while the quantitative property is rephrased as a qualitative one over the enhanced model. However, such a quantitative-to-qualitative approach lacks generality and is prone to errors, as it makes no clear distinction between the system to be verified (the actual behavior) and the property to be checked (the desired behavior). We propose a cleaner method for discrete quantitative model-checking by extending linear temporal logic (LTL) with counting capabilities: Cost Linear Temporal Logic (CLTL). This extension can be translated into Büchi automata equipped with counters, so as to nicely extend the automata approach to model-checking. We describe the new properties that this extension allows to handle, illustrated with examples. We also explain how it is linked to existing qualitative LTL model-checking, and the new challenges it poses. -- Alexandre Duret-Lutz