# Approximation based tree regular model checking

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 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.
Keywords :
Document type :
Journal articles
Domain :

Cited literature [67 references]

https://hal.inria.fr/inria-00429345
Contributor : Pierre-Cyrille Heam <>
Submitted on : Monday, November 2, 2009 - 4:56:32 PM
Last modification on : Tuesday, October 27, 2020 - 2:34:28 PM
Long-term archiving on: : Thursday, June 17, 2010 - 7:05:14 PM

### File

Haltreermc.pdf
Files produced by the author(s)

### Identifiers

• 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⟩

Record views