LIP6 1997/017
- Reports
Une Technique Automatique de Vérification de Propriétés des Systèmes Symétriques - K. Ajami, J.-M. Ilié
- 20 pages - 09/10/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.017.ps.gz - 74 Ko
- Contact : Khalil.Ajami (at) nulllip6.fr, Jean-Michel.Ilie (at) nulllip6.fr
- Ancien Thème : SRC
- Keywords : Temporal Logic, Symmetries, Symbolic Reachability Graph, Well-formed Nets
- Publisher : Denis.Poitrenaud (at) nulllip6.fr
In this paper, we propose an automatic technique for CTL* Model checking through the Symbolic Reachability Graph (SRG). SRG is a highly condensed representation of system state space built automatically from a specification of system in terms of Well-formed net. The building of such graph profits from the presence of object symmetries to aggregate either states or actions within symbolic representatives. Our technique consists in making the formal approach of CTL* model checking presented in [1], operational. We propose a derived temporal logic CPN-CTL* (computational Temporal Logic Star) equivalent to CTL* and built to express properties of systems specified by means of a Well-formed net. We show how to perform the model checking of such a formula directly through SRG by retrieving the behavior of the objects specified within these formulas. Effectively, SRG are built according to definitions of representatives of symmetrical object groups for which the identity of objects is not preserved, i.e. only the nature of objects and the cardinality of groups are known. This technique leads to a new specification of system, from which we can prove that model checking through a state space is equivalent to model checking through the symbolic reachability graph.