LIP6 1998/020
- Rapports de recherche
Exploitation des Symétries dans la Vérification des propriétés des Systèmes Concurrents - K. Ajami, S. Haddad, J.-M. Ilié
- 21 pages - 18/05/1998- document en - http://www.lip6.fr/lip6/reports/1998/lip6.1998.020.ps.gz - 86 Ko
- Contact : Khalil.Ajami (at) nulllip6.fr, haddad (at) nulllamsade.dauphine.fr, Jean-Michel.Ilie (at) nulllip6.fr
- Ancien Thème : SRC
- Mots clés : Logique Temporelle, LTL, Symétries, Automates de Büchi, Vérification, Vérification du Modèle
- Directeur de la publication : Denis.Poitrenaud
La vérification des propriétés des systèmes concurrents peut être effectuée par la spécification et la vérification des formules de logique temporelle sur un graphe états-transition modélisant le système. Le problème connu de l'explosion combinatoire dans le temps et l'espace nécessite le développement de techniques efficaces pour réduire (par rapport à certaines propriétés) la taille du graphe à construire.
Une des techniques les plus prometteuses fut initiée par Emerson & al [6]. Cette technique exploite les symétries en se basant sur l'idée que les symétries ne sont pas détectables dans le système seulement, mais elle sont également détectables dans toute formule décrivant une propriété de ce système. La relation d'équivalence, déduite de ces symétries, appartient à un sous groupe de permutation préservant la formule et le système en même temps (l'application d'une permutation de ce sous groupe sur un état du système donne un état appartenant à la même classe. En plus, l'application d'une telle permutation sur la formule ne change pas ses valeurs de vérité). Néanmoins la précédente technique offre une méthode de vérification qui exploite les symétries d'une façon très restrictive. En effet, deux types de symétries sont détectées: les symétries propositionnelle et les symétries globales par rapport à un sous groupe de symétries qui opèrent sur une structure représentant la formule.
Notre but est de généraliser la notion de symétrie proposée ci-dessus. Ceci peut être fait par l'exploitation plus fine des symétries locales exprimées sur des chemins d'une formule CTL*. Notre approche consiste à analyser l'automate de Büchi construit sur des séquences pour les formules LTL. Les automates considérées ne sont pas nécessairement symétrique d'une façon globale par rapport à un groupe de symétrie. En effet, à partir d'un automate on détermine l'ensemble des symétries entre ses états en considérant que deux états d'un automates sont symétriques s'ils représentent le même comportement courant et futur par
rapport à une permutation de processus. Pour une permutation, cette relation peut être calculée en un temps polynomiale.De la même façon on détecte, dans le modèle représentant le système, les symétries du modèle en considérant que deux états sont symétriques s'il sont égaux à une permutation près calculées selon les valeurs courantes des
variables du système.
En appliquant ces relations sur le produit synchrone de l'automate et du graphe qui modélise le système, on définit une structure quotient. On prouve que la vérification utilisant cette approche est équivalent à la vérification utilisant la formule et le graphe complet. Néanmoins, le calcul général des permutations a une complexité exponentiel ce qui réduit en quelques sorte les bénéfices réalisés par la réduction du graphe. Cependant, on propose une approche alternative qui calcule dans un temps polynomiale une structure avec une taille intermédiaire. Cette structure a les mêmes propriétés d'équivalence de la structure quotient et réalise dans des cas pratiques des réductions exponentielles.
Une des techniques les plus prometteuses fut initiée par Emerson & al [6]. Cette technique exploite les symétries en se basant sur l'idée que les symétries ne sont pas détectables dans le système seulement, mais elle sont également détectables dans toute formule décrivant une propriété de ce système. La relation d'équivalence, déduite de ces symétries, appartient à un sous groupe de permutation préservant la formule et le système en même temps (l'application d'une permutation de ce sous groupe sur un état du système donne un état appartenant à la même classe. En plus, l'application d'une telle permutation sur la formule ne change pas ses valeurs de vérité). Néanmoins la précédente technique offre une méthode de vérification qui exploite les symétries d'une façon très restrictive. En effet, deux types de symétries sont détectées: les symétries propositionnelle et les symétries globales par rapport à un sous groupe de symétries qui opèrent sur une structure représentant la formule.
Notre but est de généraliser la notion de symétrie proposée ci-dessus. Ceci peut être fait par l'exploitation plus fine des symétries locales exprimées sur des chemins d'une formule CTL*. Notre approche consiste à analyser l'automate de Büchi construit sur des séquences pour les formules LTL. Les automates considérées ne sont pas nécessairement symétrique d'une façon globale par rapport à un groupe de symétrie. En effet, à partir d'un automate on détermine l'ensemble des symétries entre ses états en considérant que deux états d'un automates sont symétriques s'ils représentent le même comportement courant et futur par
rapport à une permutation de processus. Pour une permutation, cette relation peut être calculée en un temps polynomiale.De la même façon on détecte, dans le modèle représentant le système, les symétries du modèle en considérant que deux états sont symétriques s'il sont égaux à une permutation près calculées selon les valeurs courantes des
variables du système.
En appliquant ces relations sur le produit synchrone de l'automate et du graphe qui modélise le système, on définit une structure quotient. On prouve que la vérification utilisant cette approche est équivalent à la vérification utilisant la formule et le graphe complet. Néanmoins, le calcul général des permutations a une complexité exponentiel ce qui réduit en quelques sorte les bénéfices réalisés par la réduction du graphe. Cependant, on propose une approche alternative qui calcule dans un temps polynomiale une structure avec une taille intermédiaire. Cette structure a les mêmes propriétés d'équivalence de la structure quotient et réalise dans des cas pratiques des réductions exponentielles.