Tree Pattern Rewriting Systems

  • Blaise Genest
  • Anca Muscholl
  • Olivier Serre
  • Marc Zeitoun
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)


Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XML-based applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XML-based documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system \((T,{\mathcal R})\), a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T.


Turing Machine Tree Pattern Service Call Level Counter Semistructured Data 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321. IEEE Comp. Soc, Los Alamitos (1996)Google Scholar
  2. 2.
    Abiteboul, S., Benjelloun, O., Milo, T.: Positive Active XML. In: PODS 2004, pp. 35–45. ACM, New York (2004)Google Scholar
  3. 3.
    Abiteboul, S., Segoufin, L., Vianu, V.: Analysis of Active XML Services. In: PODS 2008. ACM Press, New York (to appear, 2008)Google Scholar
  4. 4.
  5. 5.
    Chambart, P., Schnoebelen, P.: The Ordinal Recursive Complexity of Lossy Channel Systems. In: LICS 2008, pp. 205–216. IEEE Comp. Soc., Los Alamitos (2008)Google Scholar
  6. 6.
    R. Diestel. Graph theory (2005),
  7. 7.
    Dufourd, C., Finkel, A., Schnoebelen, P.: Reset Nets between Decidability and Undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. 8.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere. Theor. Comput. Sci. 256(1-2), 63–92 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Genest, B., Muscholl, A., Serre, O., Zeitoun, M.: Tree Pattern Rewrite Systems. Internal report,
  10. 10.
    Dershowitz, N., Plaisted, D.: In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 9, vol. 1. Elsevier, Amsterdam (2001)Google Scholar
  11. 11.
    Libkin, L.: Logics over unranked trees: an overview. Logical Methods in Computer Science 2(3) (2006)Google Scholar
  12. 12.
    Löding, C., Spelten, A.: Transition Graphs of Rewriting Systems over Unranked Trees. In: Kučera, L., Kučera, A. (eds.) MFCS 2007. LNCS, vol. 4708, pp. 67–77. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Neven, F.: Automata, Logic, and XML. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 2–26. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Schnoebelen, P.: Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Inf. Process. Lett. 83(5), 251–261 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Walukiewicz, I.: Difficult Configurations—on the Complexity of LTrL. ICALP 1998 26(1), 27–43 (2005); In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 27–43. Springer, Heidelberg (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Blaise Genest
    • 3
  • Anca Muscholl
    • 1
  • Olivier Serre
    • 2
  • Marc Zeitoun
    • 1
  1. 1.LaBRI, BordeauxFrance
  2. 2.LIAFA, Paris 7 & CNRSFrance
  3. 3.IRISA, Rennes 1 & CNRSFrance

Personalised recommendations