Projet ANR-11-BS02-0001 – REACHARD : Problèmes d'accessiblité difficiles pour les systèmes à compteurs
Programme : Blanc - SIMI 2 - Science informatique et applications (Blanc SIMI 2)
Année de financement : 2011
Coordinateur du projet : Monsieur Alain FINKEL (CNRS - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR EST)
Partenaires : Laboratoire Spécification et Vérification; Laboratoire Bordelais de Recherche en Informatique
Montant : 262818.0 euros
Date de début : 2011
Durée : 36 mois
Résumé : ReacHardIl s'agit d'étudier les problèmes d'accessibilité dans les systèmes à compteurs.
Analyser la structure des ensembles d'accessibilités et la complexité des structures impliquées.L'algorithme de décision pour l'accessibilité dans les VASS n'a jamais été mis en œuvre. C'est en raison de sa grande complexité, à la fois conceptuelle (l'algorithme est très difficile à comprendre et à décrire) et de calcul (on suppose que la complexité de l'algorithme n'est pas primitive récursive). En fait,on peut dire que le problème n'est toujours pas résolu de façon satisfaisante. L'objectif principal du projet est de proposer une solution satisfaisante au problème de l'accessibilité pour les systèmes d'addition de vecteurs.
Outils algébriques, logiques et de complexitéNous avons utilisé des outils algébriques, géométriques, logiques et de complexité pour résoudre les problèmes d'accessibilité. Par exemple, les ensembles définissables par des logiques sont aussi vus comme satisfaisant des systèmes d'équations, et associés à des espaces vectoriels. La complexité de ces structures est aussi étudiée. Cela a permis de caractériser la complexité des beaux ordres les plus courants.
Résumé de la soumission : Contexte:Depuis leur invention au début des années 1980, les techniques devérification de modèles (model-checking en anglais) sontdevenues incontournables pour la vérification automatique de systèmesinformatiques, qu'il s'agisse de circuits électroniques, de protocoles decommunication ou d'algorithmes. Ces techniques sont appliquées àtoutes les étapes de conception, des spécifications abstraites à hautniveau aux logiciels effectivement déployés. Les trente dernièresannées ont vu ces techniques être continuellement adaptées à denouveaux types de systèmes, et leur principale limitation -- à savoirl'explosion du nombre d'états -- a été combattue et contenue par lamise au point de nouvelles approches de modélisation, techniquesd'abstraction, algorithmes dédiés, et structures de données efficaces.Le cas des systèmes à compteurs est typique des approches pour lavérification de systèmes infinis. Ces systèmes à compteursapparaissent encore et encore, dans les modélisations de protocolesdistribués, de programmes parallélisés, de programmes avec pointeurs,de protocoles de diffusion multipoints, de bases de données, etc. Lesprincipaux résultats en matière de vérification de systèmes àcompteurs sont l'indécidabilité dans le cas où des tests à zéro descompteurs sont possibles, et a contrario la décidabilité de plusieursproblèmes quand de tels tests sont interdits -- on parle alors deVASS, pour « systèmes d'addition de vecteurs », ou de manièreéquivalente de réseaux de Petri. La preuve de décidabilité del'accessibilité dans les VASS de 1982 fait de ce problème unproblème-pivot en informatique théorique, puisque ses applicationsdépassent largement la vérification de la sûreté des systèmes àcompteurs pour inclure des problèmes dans des domaines de recherchetrès actifs sur des logiques, des automates sur des mots ou des arbresavec données. De ce fait, la mise au point d'algorithmes efficacespour ce problème d'accessibilité aurait un impact important au-delà dudomaine de la vérification de systèmes. Toute diminution des besoinsen temps et en espace mémoire nécessaires pour résoudre ce problèmed'accessibilité dans les VASS se répercuterait aussitôt dans quantitéd'autres domaines.Objectifs principaux:Étonnamment, l'algorithme permettant de décider l'accessibilité dansles VASS n'a jamais été mis en œuvre en pratique. Cela s'explique parson énorme complexité, tant conceptuelle (l'algorithme est trèsdifficile à comprendre et à décrire) que calculatoire (il estadmis que la complexité de l'algorithme n'est pas primitivementrécursive). Il est en fait raisonnable de dire que le problème n'estpas résolu de manière pleinement satisfaisante.L'objectif principal du projet est d'obtenir une telle solutionsatisfaisante. Des avancées récentes sur le sujet et sur des problèmesproches, dont plusieurs obtenues par des participants du projet, nouspermettent aussi d'avancer des solutions pour des extensions, commepar exemple des VASS avec un seul test à zéro ou des VASSarborescents. Nous bénéficions aussi d'une nouvelle preuve dedécidabilité, qui introduit par exemple une notion de séparateurssemi-linéaires qui pourraient être mis en œuvre concrètement. Grâce àl'expertise des différents partenaires et des participants au LaBRI etau LSV, nous proposons de développer des techniques nouvelles pourmieux cerner la structure mathématique des ensembles d'accessibilité,de mener à bout une analyse calculatoire des problèmes d'accessibilitédes VASS, et de mettre au point de nouveaux algorithmes. Tous lesparticipants du projet sont aussi impliqués dans la rédaction d'une monographie sur lessystèmes à compteurs, largement axée sur les problèmes d'accessibilitédans les VASS. Cet ouvrage sera un des principaux livrables du projet.
Résultats : Nos recherches ont proposé de nouveaux algorithmes d’accessibilité dans les machines à compteurs et en ont précisé les complexités ; elles vont donc faciliter la vérification des machines à compteurs associées à des protocoles et programmes, comme le protocole TTP qui assure la cohérence du freinage sur les quatre roues d’une voiture. De nouveaux partenariats internationaux ont vus le jour : une collaboration avec les chercheurs de la Chaire DIGITEO et une autre avec le Professeur Ranko Lazic de l’Université de Warwick.
Donnons un exemple: Leroux a répondu positivement à la conjecture énoncée dans la tâche 4.1. Il montre que les techniques d'accélération sont complètes pour le calcul de l'ensemble des états accessibles d'un VAS semilinéaire.
La liste des autres résultats est dans le rapport complet et trop longue pour être copiée ici.
Perspectives : Outre l’exploitation académique des résultats apparaissant déjà dans ce rapport (publications, conférences, écoles, collaborations,…), les deux derniers résultats théoriques méritent d’être détaillés : début janvier 2015, deux des membres du projet ReacHard ont trouvé la première borne de complexité au problème de l’accessibilité dans les VASS et deux autres membres du projet ReacHard ont trouvé la complexité exacte de l’accessibilité pour les VASS de dimension deux Ces deux problèmes étaient ouverts depuis plus de 30 ans.
Ces résultats nous ont motivé à commencer (début janvier 2015), avec des partenaires de la Chaire DIGITEO (Université de Montréal, Canada), la construction d’un prototype pour vérifier l’accessibilité dans un VASS de dimension quelconque.
Donnons un exemple parmi d'autres: nous nous attaquons maintenant à la détection de la semilinéarité. Cette caractérisation devrait permettre de construire des algorithmes pour décider le problème général de l'accessibilité pour les VAS non semilinéaires. Nous allons travailler sur la complexité de décider le problème du context-freeness d'un VAS.
La liste des autres perspectives est dans le rapport complet et trop longue pour être copiée ici.
Publications et brevets : Nous avons produit 11 articles dans des revues internationales et 32 papiers dans des conférences internationales. La liste est dans le rapport complet et trop longue pour être copiée ici.