Verifying Recursive Active Documents with Positive Data Tree Rewriting
Databases
2010-03-05 v1 Other Computer Science
Abstract
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 -complete.
Cite
@article{arxiv.1003.1010,
title = {Verifying Recursive Active Documents with Positive Data Tree Rewriting},
author = {Blaise Genest and Anca Muscholl and Zhilin Wu},
journal= {arXiv preprint arXiv:1003.1010},
year = {2010}
}