Skip to Main content Skip to Navigation
Journal articles

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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Complete list of metadata

Cited literature [67 references]  Display  Hide  Download
Contributor : Pierre-Cyrille Heam Connect in order to contact the contributor
Submitted on : Monday, November 2, 2009 - 4:56:32 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM
Long-term archiving on: : Thursday, June 17, 2010 - 7:05:14 PM


Files produced by the author(s)


  • HAL Id : inria-00429345, version 1


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⟩



Record views


Files downloads