Abstract
Term Rewriting Systems are now commonly used as a modeling language for programs or systems. On those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. For disproving reachability (i.e. proving non reachability of a term) on non terminating and non confluent rewriting models, Knuth-Bendix completion and other usual rewriting techniques do not apply. Using the tree automaton completion technique, it has been shown that the non reachability of a term t can be shown by computing an over-approximation of the set of reachable terms and prove that t is not in the approximation. However, when the term t is in the approximation, nothing can be said. In this paper, we refine this approach and propose a method taking advantage of the approximation to compute a rewriting path to the reachable term when it exists, i.e. produce a counter example. The algorithm has been prototyped in the Timbuk tool. We present some experiments with this prototype showing the interest of such an approach w.r.t. verification of rewriting models.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santos Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Boichut, Y., Genet, Th.: Trace reconstruction. Research Report RR2006-02, LIFC - Laboratoire d’Informatique de l’Université de Franche Comtéand IRISA / Université de Rennes (2006), http://lifc.univ-fcomte.fr/publis/papers/Year/2006.html
Boichut, Y., Héam, P.-C., Kouchnarenko, O.: Automatic Verification of Security Protocols Using Approximations. Research Report RR-5727, INRIA-Lorraine - CASSIS Project (October 2005)
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E., Ringeissen, C.: An overview of f elan. In: Proc. 2nd WRLA, Pont-à-mousson (France). ENTCS. Elsevier, Amsterdam (1998)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science (2001)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2002), http://www.grappa.univ-lille3.fr/tata/
Feuillade, G., Genet, T., Tong, V.V.T.: Reachability Analysis over Term Rewriting Systems. JAR 33(3-4), 341–383 (2004)
Genet, T.: Decidable approximations of sets of descendants and sets of normal forms. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 151–165. Springer, Heidelberg (1998)
Gaillourdet, J.-M., Hillenbrand, T., Löchner, B., Spies, H.: The new Waldmeister loop at work. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 317–321. Springer, Heidelberg (2003)
Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831. Springer, Heidelberg (2000)
Genet, T., Tang-Talpin, Y.-M., Tong, V.V.T.: Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems. In: Proc. of WITS 2003 (2003)
Gyenizse, P., Vágvölgyi, S.: Linear Generalized Semi-Monadic Rewrite Systems Effectively Preserve Recognizability. TCS 194(1-2), 87–122 (1998)
Genet, T., Tong, V.V.T.: Timbuk 2.0 – a Tree Automata Library. IRISA / Université de Rennes 1 (2000), http://www.irisa.fr/lande/genet/timbuk/
Genet, T., Tong, V.V.T.: Reachability Analysis of Term Rewriting Systems with timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 695–702. Springer, Heidelberg (2001)
Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)
Monniaux, D.: Abstracting Cryptographic Protocols with Tree Automata. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, p. 149. Springer, Heidelberg (1999)
Oehl, F., Cécé, G., Kouchnarenko, O., Sinclair, D.: Automatic Approximation for the Verification of Cryptographic Protocols. In: Proceedings of FASE 2003. LNCS, vol. 2629, pp. 34–48. Springer, Heidelberg (2003)
Takai, T., Kaji, Y., Seki, H.: Right-linear finite-path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boichut, Y., Genet, T. (2006). Feasible Trace Reconstruction for Rewriting Approximations. In: Pfenning, F. (eds) Term Rewriting and Applications. RTA 2006. Lecture Notes in Computer Science, vol 4098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11805618_10
Download citation
DOI: https://doi.org/10.1007/11805618_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-36834-2
Online ISBN: 978-3-540-36835-9
eBook Packages: Computer ScienceComputer Science (R0)