The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Un système d'étiquetage pour une propriété P dans une structure consiste à assigner à chaque élément du domaine une étiquette, aussi petite que possible, de telle sorte que l'on puisse vérifier la propriété en ne regardant que les étiquettes. Les systèmes d'étiquetage peuvent être vus comme un pré-traitement en vu de faire du model checking. En model-checking les objets manipulés sont le plus souvent statiques. Lorsque la structure est modifiée dans le temps, on refait tous les calculs. Nous nous intéressons aux structures qui peuvent perdre des sommets/relations. Nous voulons pouvoir répondre, de manière rapide à n'importe quel moment, si le graphe résultant après suppression de sommets/arêtes vérifie une propriété P. Notre technique consiste à utiliser les systèmes d'étiquetage. Je montrerai comment vérifier des propriétés du premier ordre dans certaines classes de graphes en utilisant des étiquettes de taille logarithmique (les étiquettes sont calculées une seule fois). Un ingrédient principal est le résultat de Gaifman et une décomposition des formules locales de Frick. Ces résultats peuvent être étendus au comptage.