Tree pattern rewriting systems

Blaise Genest, Anca Muscholl, Olivier Serre, Marc Zeitoun

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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 , 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.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings
PublisherSpringer Verlag
Pages332-346
Number of pages15
ISBN (Print)354088386X, 9783540883869
DOIs
Publication statusPublished - 1 Jan 2008
Externally publishedYes
Event6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008 - Seoul, Korea, Republic of
Duration: 20 Oct 200823 Oct 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5311 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008
Country/TerritoryKorea, Republic of
CitySeoul
Period20/10/0823/10/08

Fingerprint

Dive into the research topics of 'Tree pattern rewriting systems'. Together they form a unique fingerprint.

Cite this