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 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.
Complete list of metadatas

Cited literature [67 references]  Display  Hide  Download

https://hal.inria.fr/inria-00429345
Contributor : Pierre-Cyrille Heam <>
Submitted on : Monday, November 2, 2009 - 4:56:32 PM
Last modification on : Thursday, February 7, 2019 - 3:46:32 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⟩

Share

Metrics

Record views

842

Files downloads

140