Property-Dependent Reductions for the Modal Mu-Calculus

Radu Mateescu 1 Anton Wijs 2
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Résumé : Lorsqu'on analyse le comportement des systèmes concurrents à espace d'états fini par model checking, une manière de lutter contre l'explosion d'états est de réduire le modèle le plus possible tout en préservant les propriétés à vérifier. Nous considérons le cadre des systèmes basés sur actions, dont les comportements peuvent être représentés par des systèmes de transitions étiquetées (STEs), et dont les propriétés temporelles d'intérêt peuvent être formulées en mu-calcul modal (Lmu). D'abord, nous déterminons, pour toute formule de Lmu, l'ensemble maximal des actions qui peuvent être masquées dans le STE sans changer l'interprétation de la formule. Ensuite, nous définissons dsbrLmu, un fragment de Lmu qui est compatible avec la bisimulation de branchement sensible à la divergence. Ceci permet d'appliquer le masquage maximal et de réduire le STE à la volée en utilisant la tau-confluence sensible à la divergence pendant la vérification de la formule dsbrLmu. Les expériences que nous avons effectuées sur différents exemples de protocoles de communication et de systèmes distribués montrent que cette approche de réduction peut améliorer de manière significative les performances de la vérification à la volée.
Type de document :
Rapport
[Research Report] RR-7690, INRIA. 2011, pp.30
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00609585
Contributeur : Radu Mateescu <>
Soumis le : mardi 19 juillet 2011 - 14:41:11
Dernière modification le : jeudi 11 janvier 2018 - 01:48:48
Document(s) archivé(s) le : jeudi 20 octobre 2011 - 02:25:34

Fichier

RR-7690.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00609585, version 1

Citation

Radu Mateescu, Anton Wijs. Property-Dependent Reductions for the Modal Mu-Calculus. [Research Report] RR-7690, INRIA. 2011, pp.30. 〈inria-00609585〉

Partager

Métriques

Consultations de la notice

145

Téléchargements de fichiers

76