2010/03/04 by Blaise Genest, Genest, Blaise, Anca Muscholl +3
Computer Science · #Advanced Data Storage Technologies #Advanced Database Systems and Queries #Databases (cs.DB) #FOS: Computer and information sciences #Other Computer Science (cs.OH) #Semantic Web and Ontologies #cs.DB #cs.OH
paper · pdf · doi:10.48550/arxiv.1003.1010
arxiv created 2010/03/04 · openalex publication_date 2010/03/04 · arxiv updated 2010/03/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This paper proposes a data tree-rewriting framework for modeling evolving documents. The framework is close to Guarded Active XML, a platform used for handling XML repositories evolving through web services. We focus on automatic verification of properties of evolving documents that can contain data from an infinite domain. We establish the boundaries of decidability, and show that verification of a \em positive fragment that can handle recursive service calls is decidable. We also consider bounded model-checking in our data tree-rewriting framework and show that it is \nexptime-complete.