LIP6 1998/020
- Reports
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 - 05/18/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
- Keywords : Temporal Logic, Symmetries, Büchi Automata, Model Checking
- Publisher : Denis.Poitrenaud
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.