Implémentation d'Algorithmes pour l'Analyse des SAVE de Dimension Deux

Lieu : LaBRI (Laboratoire Bordelais de Recherche en Informatique), Université de Bordeaux, France
Équipe : Méthodes et Modèles Formels / Modèles et Technologies pour la Vérification
Encadrants : Jérôme Leroux et Grégoire Sutre
Mots-clés : Problème d'Atteignabilité, Systèmes d'Addition de Vecteurs, Vérification de Modèles, Ensembles Semilinéaires, Arithmétique de Presburger
Durée : 6 semaines

Sujet

Les systèmes d'addition de vecteurs avec états (SAVE) sont des automates finis équipés de compteurs, à valeurs dans les entiers naturels, pouvant être incrémentés et décrementés. Ce modèle a été introduit par Karp et Miller dans les années 1960 [1], et a depuis fait l'objet de nombreux travaux de recherche. Les SAVE peuvent sembler relativement simples à première vue, mais les comportements qu'ils induisent sont en réalité très complexes. L'un des problèmes de décision les plus élémentaires pour les SAVE est l'atteignabilité : étant donné un SAVE et deux configurations de ce SAVE, la seconde configuration est-elle atteignable depuis la première ? Ce problème a été montré décidable dans les années 1980, mais sa complexité algorithmique exacte n'a été établie qu'en 2021.

Une des premières sous-classes de SAVE pour lesquelles l'atteignabilité a été montrée décidable est la classe des SAVE de dimension deux. Pour cette classe, Hopcroft et Pansiot ont conçu un algorithme qui calcule une description finie (plus précisément une présentation semilinéaire) de l'ensemble des configurations atteignables [2]. Une conséquence immédiate de ce résultat est que l'atteignabilité est décidable pour cette classe.

L'objectif de ce stage est d'implémenter un algorithme similaire à celui d'Hopcroft et Pansiot pour une extension dite branchante des SAVE de dimension deux. Cet algorithme effectue de nombreuses opérations sur les ensembles linéaires de dimension deux. La première étape du stage consistera donc à implémenter une petite bibliothèque pour la manipulation efficace d'ensembles linéaires de dimension deux.

Références

  1. R. M. Karp and R. E. Miller. “Parallel Program Schemata”. In: Journal of Computer and System Sciences 3.2 (1969), pp. 147–195.
  2. J. Hopcroft and J.-J. Pansiot. “On the reachability problem for 5-dimensional vector addition systems”. In: Theoretical Computer Science 8.2 (1979), pp. 135–159.