Approximation based tree regular model checking

Yohan Boichut 1 Pierre-Cyrille Heam 2, 3 Olga Kouchnarenko 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper addresses the following general problem of tree regular model-checking: decide whether $\R^*(L)\cap L_p =\emptyset$ where $\R^*$ is the reflexive and transitive closure of a successor relation induced by a term rewriting system $\R$, and $L$ and $L_p$ are both regular tree languages. We develop an automatic approximation-based technique to handle this -- undecidable in general -- problem in most practical cases, extending a recent work by Feuillade, Genet and Viet Triem Tong. We also make this approach fully automatic for practical validation of security protocols.
Type de document :
Article dans une revue
Nordic Journal of Computing, Publishing Association Nordic Journal of Computing, 2008, 14, pp.216-241
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00429345
Contributeur : Pierre-Cyrille Heam <>
Soumis le : lundi 2 novembre 2009 - 16:56:32
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13
Document(s) archivé(s) le : jeudi 17 juin 2010 - 19:05:14

Fichier

Haltreermc.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00429345, version 1

Citation

Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko. Approximation based tree regular model checking. Nordic Journal of Computing, Publishing Association Nordic Journal of Computing, 2008, 14, pp.216-241. 〈inria-00429345〉

Partager

Métriques

Consultations de la notice

341

Téléchargements de fichiers

107