ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 27/1-2 - 2008  - pp.7-28  - doi:10.3166/tsi.27.7-28
TITRE
Clôtures transitives de semi-commutations et model-checking régulier

RÉSUMÉ
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.


ABSTRACT
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.


AUTEUR(S)
G. CÉCÉ, P.-C. HÉAM, Y. MAINIER

Reçu le 14 octobre 2004.    Accepté le 15 septembre 2005.

MOTS-CLÉS
model checking régulier, vérification, systèmes paramétrés, semi-commutations.

KEYWORDS
regular model checking, verification, parametric systems, semi-commutations.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (367 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier