Algorithme de complétion d’automates d’arbres . . .

EXEMPLE 

Considérons le protocole de passage de jeton entre plusieurs processus placés les uns à la suite des autres. Chacun de ces processus peut être soit en repos, soit en section critique, selon qu’il possède ou non l’unique jeton disponible. Et chaque processus peut passer le jeton à son voisin de droite. Un état courant de ce protocole (pour un nombre de processus fini) peut alors être représenté par un mot sur l’alphabet {N, T} où N représente un processus au repos, et T représente un processus possédant le jeton. Pour représenter une configuration (ou état) courante de ce protocole pour un nombre indéterminé (donc potentiellement infini) de processus, nous allons utiliser un automate de mot. En figure 2.1, est représenté l’ensemble des configurations dans laquelle le deuxième processus possède le jeton (quelque soit le nombre de processus).

Termes

Continuons maintenant avec les termes, construits depuis un alphabet de symboles fonctionnels et pouvant se représenter sous forme d’arbres.

DÉFINITION (Alphabet de symboles fonctionnels)

Un alphabet F est un alphabet de symboles fonctionnels si chacun de ses symboles possède une arité (i.e. un entier positif ou nul). F 0 est l’ensemble des constantes (symboles d’arité 0) de F et F n l’ensemble des symboles d’arité n.
Un élément construit sur un alphabet F est appelé un terme, et peut se représenter sous forme d’arbre : les feuilles sont les symboles d’arité 0, et chaque symbole d’arité k possède k fils.

DÉFINITION  (Règle et système de réécriture linéaire, linéaire droit(e), linéaire gauche)

Une règle de réécriture l → r est linéaire gauche (respectivement linéaire droite) si l (respectivement r) est linéaire. Un système de réécriture est linéaire gauche (respectivement linéaire droit) si toutes ses règles de réécriture sont linéaires gauches (respectivement linéaires droites). Une règle (ou un système) de réécriture est linéaire si elle (il) est linéaire gauche et linéaire droit(e).

Automates d’arbres

Définissons maintenant les automates d’arbres, dont le langage est un ensemble (possiblement infini) de termes. Dans la modélisation d’un système informatique par un automate d’arbres, un terme permet de représenter une configuration (ou état) du système, et un automate d’arbres permet de représenter un ensemble de configurations (possiblement infini). Soient F un alphabet de symboles fonctionnels et Q un ensemble fini de symboles d’arité 0, appelés états, tels que Q ∩ F = ∅. T (F ∪ Q) est l’ensemble des configurations sur F. Il est défini inductivement comme suit.

Model-Checking régulier sur arbres

Comme expliqué brièvement dans l’introduction, cette thèse se place principalement dans le cadre de la vérification de propriétés de sûreté. Rappelons succinctement qu’une propriété de sûreté consiste à spécifier qu’un système ne peut jamais atteindre une mauvaise configuration. On appelle alors ceci un problème d’atteignabilité. Pour cela, il faut tout d’abord calculer l’ensemble des configurations atteignables par un système afin de vérifier qu’aucune mauvaise configuration n’y est présente. Le Model-Checking consiste alors à modéliser un système en séparant la modélisation de ses différentes configurations (ou états), et les actions permettant de passer d’une configuration à une autre (i.e., ses transitions). Cette modélisation est appelée système état-transition.
Dans le cas de systèmes à ensembles d’états infinis, le premier problème difficile qui se pose est le suivant : comment représenter et manipuler des ensembles infinis d’états ? Pour résoudre ce problème récurrent en vérification, il n’existe que des solutions partielles. La solution proposée par le Model-Checking régulier est basée sur les langages réguliers de mots (Regular Model-Checking : RMC [Bouajjani et al., 2000]), ou sur les langages réguliers de termes ( Regular Tree Model-Checking : RTMC [Abdulla et al., 2002]).
Le Model-Checking régulier sur mots ou arbres respecte le formalisme du système état-transition. En effet, on a alors :
– un état (ou configuration) du système est représentée par un mot ou un terme,
– un ensemble d’états (potentiellement infini) est représenté par un automate de mots ou un automate d’arbres,
– et la fonction de transition (ou fonction successeur) modélisant le comportement du système à vérifier (et permettant donc de passer d’une configuration à une autre, i.e., d’un automate d’arbres à un autre) est représentée par un transducteur (dans le cas des mots), par un système de réécriture ou un transducteur d’arbres (dans le cas des arbres).
Nous utiliserons dans cette thèse les automates d’arbres comme représentation des ensembles d’états et les systèmes de réécritures en tant que fonction de transition. Le RMC (Model-Checking régulier sur mots) et les transducteurs d’arbres seront définis et comparés en section 3.2.1. Soit A0 l’automate d’arbres représentant l’ensemble des configurations initiales du système, R le système de réécriture représentant le comportement du système à modéliser et F l’alphabet du système. Dans le cadre du système état-transition, on a alors :
Ce calcul est le but de l’algorithme de complétion que nous allons décrire en section suivante. Il est intéressant de noter que la classe des langages reconnaissables par automates d’arbres est close par intersection (∩) et cette opération s’effectue en temps polynomial pour deux automates. En effet, l’intersection entre deux automates A1 et A2 possède une complexité en O(||A1|| × ||A2||) (où ||Ai
|| est la taille de l’automate Ai [Comon et al., 2007]). Par ailleurs, la décision du vide, consistant à déterminer si le langage d’un automate d’arbres est vide ou non, est une opération décidable s’effectuant en temps linéaire. Les automates d’arbres sont donc tout à fait adaptés pour la vérification de propriété de sûreté, puisqu’il suffit de vérifier que L(Af ) ∩ Bad = ∅, si Bad est un ensemble de termes régulier.

Algorithme de complétion d’automates d’arbres

Dans cette section, nous allons décrire la méthode utilisée et étendue tout au long de cette thèse, permettant de calculer l’ensemble des configurations accessibles d’un système (ou une sur-approximation de cet ensemble). L’algorithme de complétion permet en effet, à partir d’un automate d’arbres représentant l’ensemble des configurations initiales du système, d’appliquer successivement un système de réécriture jusqu’à atteindre un automate reconnaissant (une sur-approximation de) l’ensemble des configurations accessibles. Ici nous allons décrire l’algorithme de complétion définit dans [Genet et Rusu, 2010].
Chaque étape i de l’algorithme de complétion consiste à appliquer un système de réécriture R sur l’automate courant que l’on va noter Ai R. Ceci va permettre d’enrichir le langage de Ai R (et ainsi ajouter les configurations découlant de ses actions ou comportement), et calculer l’automate successeur A i+1 R . La complétion de Ai R se fait par l’ajout de nouvelles transitions.
L’algorithme de complétion consiste, depuis un automate initial A0, à itérer les étapes de calcul d’automates successeurs (A1 R, A2 R, . . . : voir figure 2.7) jusqu’à obtenir un automate que l’on appelle point-fixe, i.e. un automate Ak R tel que Ak R = A k+1 R pour k ≥ 0. On dit aussi que le langage d’un automate point-fixe est R-clos, i.e. qu’il respecte la définition suivante.

Résolution des paires critiques

Maintenant que nous savons calculer l’ensemble des paires critiques d’un automate A et d’un système de réécriture R grâce à l’algorithme de filtrage, nous pouvons nous intéresser à la résolution de ces paires critiques, c’est-à-dire compléter l’automate courant pour enrichir son langage, dans le but d’obtenir un automate contenant tous les termes accessibles. Dans l’algorithme de complétion proposé par [Genet et Rusu, 2010], pour chaque paire critique hrσ, qi ∈ P C(A, R), l’automate A  est ajoutée afin de garder un historique des différentes étapes de complétion dans l’ensemble des transitions, et permet plus de précision lors de l’étape d’approximation (voir section Abstraction équationnelle). La résolution des paires critiques est résumée en figure 2.11.
Nous allons désormais nous intéresser à la manière dont va être ajouté l’ensemble de transitions nécessaire pour avoir rσ →∗ q 0 dans l’automate successeur. En effet, rappelons qu’un automate doit être composé de transitions normalisées (voir définition 2.2.2). Si rσ → q 0 n’est pas une transition normalisée (comme par exemple f(g(q)) → q 0 ), elle ne peut pas être ajoutée telle quelle dans l’ensemble de transitions d’un automate. La normalisation d’une transition consiste à la décomposer en plusieurs transitions normalisées, et ceci nécessite souvent l’utilisation de nouveaux états, comme nous allons le voir dans la définition suivante.