Special Issue – Reachability Problems (RP 2008)No Access

HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA

YOHAN BOICHUT

LIFO Bat. 3IA Université d'Orléans Rue Léonard de Vinci B.P. 6759 F-45067 ORLEANS, France

Search for more papers by this author

ROMEO COURBIS

INRIA-CASSIS LIFC, Université de Franche-Comté, 16 route de Gray, 25000 Besançon, France

Search for more papers by this author

PIERRE-CYRILLE HEAM

LSV, CNRS-INRIA, Ecole Normale Supérieure de Cachan, 61 avenue du Président Wilson, 94230 Cachan, France

Search for more papers by this author

, and

OLGA KOUCHNARENKO

INRIA-CASSIS LIFC, Université de Franche-Comté, 16 route de Gray, 25000 Besançon, France

Search for more papers by this author

https://doi.org/10.1142/S0129054109006917Cited by:1 (Source: Crossref)

Abstract

This paper addresses the following general problem of tree regular model-checking: decide whether where is the reflexive and transitive closure of a successor relation induced by a term rewriting system , and and are both regular tree languages. We develop an automatic approximation-based technique to handle this – undecidable in general – problem in the case when term rewriting system rules are non left-linear.

This work was granted by the French ANR project RAVAJ.

Keywords:

References

P. A. Abdullaet al., Computer Aided Verification, Lecture Notes in Computer Science 2404, eds. E. Brinksma and K. G. Larsen (Springer-Verlag, 2002) pp. 555–568. Crossref, Google Scholar
F. Baader and T. Nipkow , Term Rewriting and All That ( Cambridge University Press , 1998 ) . Crossref, Google Scholar
Y. Boichut et al. , Finer is better: Abstraction refinement for rewriting approximations , RTA'08, 19th int. conf. on Rewriting Techniques and Applications , LNCS ( 2008 ) . Google Scholar
Y. Boichutet al., Rewriting approximations for fast prototyping of static analyzers, Term Rewriting and Applications, 18th International Conference, RTA 20074533, LNCS, ed. Franz Baader (Springer, 2007) pp. 48–62. Google Scholar
Y. Boichut, P.-C. Héam, and O. Kouchnarenko. Automatic Verification of Security Protocols Using Approximations. Technical Report RR-5727, INRIA, 2005 . Google Scholar
Y. Boichut, P.-C. Héam and O. Kouchnarenko, Handling algebraic properties in automatic analysis of security protocols, ICTAC'064281, LNCS, eds. Kamel Barkaoui, Ana Cavalcanti and Antonio Cerone (Springer, 2006) pp. 153–167. Google Scholar
Y. Boichut and P.-C. Héam, Information Processing Letters 108(1), 1 (2008), DOI: 10.1016/j.ipl.2008.03.012. Crossref, Web of Science, Google Scholar
A. Bouajjaniet al., Abstract regular tree model checking, Infinity'05149, Electronic Notes in Theoretical Computer Science (2006) pp. 37–48. Google Scholar
A. Bouajjani and T. Touili, Computer Aided Verification, Lecture Notes in Computer Science 2404, eds. Ed Brinksma and Kim Guldstrand Larsen (Springer-Verlag, 2002) pp. 539–554. Crossref, Google Scholar
L. Bozga , Y. Lakhnech and M. Perin , Pattern-based abstraction for verifying secrecy in protocols , 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, Proceedings 2619 , LNCS ( Springer-Verlag , 2003 ) . Google Scholar
I. Cibrario et al. , Automatic detection of attacks on cryptographic protocols: A case study , Intrusion and Malware Detection and Vulnerability Assessment: Second International Conference 3548 , LNCS , eds. Christopher Kruegel and Klaus Julisch ( 2005 ) . Google Scholar
H. Comon et al. , Tree Automata Techniques and Applications ( 2002 ) . Google Scholar
J.-L. Coquidéet al., Bottom-up tree pushdown automata and rewrite systems, Rewriting Techniques and Applications, 4th International Conference, RTA-91, LNCS, ed. Ronald V. Book (Springer-Verlag, 1991) pp. 287–298. Google Scholar
V. Cortier, S. Delaune and P. Lafourcade, Journal of Computer Security 14, 1 (2006). Crossref, Web of Science, Google Scholar
M. Dauchet and S. Tison , The theory of ground rewrite systems is decidable , LICS: IEEE Symposium on Logic in Computer Science ( 1990 ) . Google Scholar
N. Dershowitz and J.-P. Jouannaud, Handbook of Theoretical Computer Science, Rewrite Systems (Elsevier Science Publishers B. V, 1990) pp. 244–320. Google Scholar
G. Feuillade, Th. Genet and V. VietTriemTong, Journal of Automated Reasonning 33(4), (2004). Google Scholar
Th. Genet and F. Klay, Rewriting for Cryptographic Protocol Verification, proceedings of CADE1831, LNCS (Springer-Verlag, 2000) pp. 271–290. Google Scholar
R. Gilleron and S. Tison, Fundamenta Informatica 24(2), 157 (1995). Crossref, Google Scholar
P. Habermehlet al., Abstract regular tree model checking of complex dynamic data structures4134, LNCS (2006) pp. 52–70. Google Scholar
J. Hopcroft and J. D. Ullman , Introduction to Automata Theory, Languages, and Computation ( Addison-Wesley , 1979 ) . Google Scholar
F. Jacquemard, Decidable approximations of term rewriting systems, proceedings of RTA1103 (Springer Verlag, 1996) pp. 362–376. Google Scholar
T. Nagaya and Y. Toyama, Decidability for left-linear growing term rewriting systems, RTA '99: Proceedings of the 10th International Conference on Rewriting Techniques and Applications (Springer-Verlag, 1999) pp. 256–270. Google Scholar
H. Ohsaki and T. Takai, Electr. Notes Theor. Comput. Sci 124(1), 97 (2005), DOI: 10.1016/j.entcs.2004.07.017. Crossref, Google Scholar
P. Réty and J. Vuotto, Electr. Notes Theor. Comput. Sci 70(6), (2002). Google Scholar
K. Salomaa, JCSS: Journal of Computer and System Sciences 37 (1988). Google Scholar