Verifying Recursive Active Documents with Positive Data Tree Rewriting

• DOI: 10.48550/arxiv.1003.1010
• Publication Date: 2010-01-01
• Authors: Blaise Genest; Anca Muscholl; Zhilin Wu
• Keywords: Tree (set theory); Fragment (logic); XPath; Well-formed document

This paper proposes a data tree-rewriting framework for modeling evolving documents. The is close to Guarded Active XML, platform used handling XML repositories through web services. We focus on automatic verification of properties documents that can contain from an infinite domain. establish the boundaries decidability, and show {\em positive} fragment handle recursive service calls decidable. also consider bounded model-checking in our it $\nexptime$-complete.