Approximation based tree regular model checking - Archive ouverte HAL Access content directly
Journal Articles Nordic Journal of Computing Year : 2008

Approximation based tree regular model checking

(1) , (2, 3) , (2)
1
2
3

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.
Fichier principal
Vignette du fichier
Haltreermc.pdf (209.12 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00429345 , version 1 (02-11-2009)

Identifiers

  • HAL Id : inria-00429345 , version 1

Cite

Yohan Boichut, Pierre-Cyrille Heam, Olga Kouchnarenko. Approximation based tree regular model checking. Nordic Journal of Computing, 2008, 14, pp.216-241. ⟨inria-00429345⟩
472 View
74 Download

Share

Gmail Facebook Twitter LinkedIn More