Problèmes d'accessiblité difficiles pour les systèmes à compteurs – REACHARD

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.

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.

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.

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.

Contexte:

Depuis leur invention au début des années 1980, les techniques de
vérification de modèles (model-checking en anglais) sont
devenues incontournables pour la vérification automatique de systèmes
informatiques, qu'il s'agisse de circuits électroniques, de protocoles de
communication ou d'algorithmes. Ces techniques sont appliquées à
toutes les étapes de conception, des spécifications abstraites à haut
niveau aux logiciels effectivement déployés. Les trente dernières
années ont vu ces techniques être continuellement adaptées à de
nouveaux types de systèmes, et leur principale limitation -- à savoir
l'explosion du nombre d'états -- a été combattue et contenue par la
mise au point de nouvelles approches de modélisation, techniques
d'abstraction, algorithmes dédiés, et structures de données efficaces.

Le cas des systèmes à compteurs est typique des approches pour la
vérification de systèmes infinis. Ces systèmes à compteurs
apparaissent encore et encore, dans les modélisations de protocoles
distribués, de programmes parallélisés, de programmes avec pointeurs,
de protocoles de diffusion multipoints, de bases de données, etc. Les
principaux résultats en matière de vérification de systèmes à
compteurs sont l'indécidabilité dans le cas où des tests à zéro des
compteurs sont possibles, et a contrario la décidabilité de plusieurs
problèmes quand de tels tests sont interdits -- on parle alors de
VASS, pour « systèmes d'addition de vecteurs », ou de manière
équivalente de réseaux de Petri. La preuve de décidabilité de
l'accessibilité dans les VASS de 1982 fait de ce problème un
problème-pivot en informatique théorique, puisque ses applications
dépassent largement la vérification de la sûreté des systèmes à
compteurs pour inclure des problèmes dans des domaines de recherche
très actifs sur des logiques, des automates sur des mots ou des arbres
avec données. De ce fait, la mise au point d'algorithmes efficaces
pour ce problème d'accessibilité aurait un impact important au-delà du
domaine de la vérification de systèmes. Toute diminution des besoins
en temps et en espace mémoire nécessaires pour résoudre ce problème
d'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é dans
les VASS n'a jamais été mis en œuvre en pratique. Cela s'explique par
son énorme complexité, tant conceptuelle (l'algorithme est très
difficile à comprendre et à décrire) que calculatoire (il est
admis que la complexité de l'algorithme n'est pas primitivement
récursive). Il est en fait raisonnable de dire que le problème n'est
pas résolu de manière pleinement satisfaisante.

L'objectif principal du projet est d'obtenir une telle solution
satisfaisante. Des avancées récentes sur le sujet et sur des problèmes
proches, dont plusieurs obtenues par des participants du projet, nous
permettent aussi d'avancer des solutions pour des extensions, comme
par exemple des VASS avec un seul test à zéro ou des VASS
arborescents. Nous bénéficions aussi d'une nouvelle preuve de
décidabilité, qui introduit par exemple une notion de séparateurs
semi-linéaires qui pourraient être mis en œuvre concrètement. Grâce à
l'expertise des différents partenaires et des participants au LaBRI et
au LSV, nous proposons de développer des techniques nouvelles pour
mieux 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 les
participants du projet sont aussi impliqués dans la rédaction
d'une monographie sur les
systèmes à compteurs, largement axée sur les problèmes d'accessibilité
dans les VASS. Cet ouvrage sera un des principaux livrables du projet.