LIP6 1998/020

Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond

K. Ajami, S. Haddad, J.-M. Ilié

LIP6 1998/020: Rapport de Recherche LIP6 / LIP6 research reports
21 pages - Mai/May 1998 - Document en anglais.

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : Exploitation des Symétries dans la Vérification des propriétés des Systèmes Concurrents
Titre anglais : Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond

Résumé : 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.

Abstract : Model checking is a useful technique to verify properties of dynamic systems but it has to cope with the state explosion problem. By simultaneous exploitation of symmetries of both the system and the property, the model checking can be performed on a reduced quotient structure [2,6,7]. In these techniques a property is specified within a temporal logic formula (CTL*) and symmetries correspond to permutations of objects which are obtained by either a syntactical checking [7] or semantical one through the state of the corresponding automaton [6]. We introduce here a more accurate method based on what we call the partial symmetries of the formula. Such symmetries are detected within the Büchi automaton of the formula and form a set of symmetries even if the fomula is not globally symmetrical i.e. there is no group of permutation (excepting the identity) operating on the formula. We define an appropriate quotient structure for the synchronized product of the Büchi automaton and the global state transition graph. We prove that model checking can be performed over this quotient structure leading to efficient algorithms.

Mots-clés : Logique Temporelle, LTL, Symétries, Automates de Büchi, Vérification, Vérification du Modèle

Key-words : Temporal Logic, Symmetries, Büchi Automata, Model Checking

Publications internes LIP6 1998 / LIP6 research reports 1998

Responsable Éditorial / Editor
webmaster@lip6.fr