Clôtures transitives de semi-commutations et model-checking régulier
Le model-checking régulier a été largement étudié ces dernières années pour l'exploration, par semi-algorithmes, de l'ensemble des configurations accessibles de systèmes paramétrés ou ayant une infinité de configurations accessibles. (Bouajjani et al., 2001; 2007) ont prouvé par une approche basée sur les expressions régulières qu'une classe particulière de langages réguliers, appelée APC, est effectivement close sous toutes les relations de semicommutations. Nous avons montré dans (Cécé et al., 2004) qu'une approche utilisant les automates est plus efficace pour les calculs et nous avons proposé une classe, PolC, stable par semi-commutation et plus large que les APC. Nous nous intéressons ici à l'utilisation de ces résultats pour des systèmes concrets dont les configurations ne font pas forcément partie de classes stables par toutes les relations de semi-commutations comme les APC ou PolC.
Last years, regular model-checking has been widely used to explore, by semialgorithms, the reachability sets of infinite states systems. (Bouajjani et al., 2001; 2007) proved, by an approach based on regular expressions, that a class of regular languages, called APC, is effectively closed under all semi-commutation relations. We presented in (Cécé et al., 2004) an approach based on automata which produces a simpler and more efficient algorithm which furthermore works for a larger class, PolC, of regular languages closed under semi-commutation relations. In this paper, we investigate the application of this last approach to concrete systems whose sets of states do not necesseraly belong to a class stable by all semi-commutation relations like APC or PolC.
G.CÉCÉ, P.HÉAM, Y.MAINIER
Reçu le 14 octobre 2004.
Accepté le 15 septembre 2005.
model checking régulier, vérification, systèmes paramétrés, semi-commutations.
regular model checking, verification, parametric systems, semi-commutations.
Français
|
