Verifying Recursive Active Documents With Positive Data Tree Rewriting
This paper considers a tree-rewriting framework for modeling documents evolving through service calls. The authors focus on the automatic verification of properties of documents that may contain data from an infinite domain. Their establish the boundaries of decidability: while verifying documents with recursive calls is undecidable, they obtain decidability as soon as either documents are in the positive-bounded fragment (while calls are unrestricted), or when there is a bound on the number of service calls (bounded model-checking of unrestricted documents). In the latter case, the complexity is NexpTime-complete. Their data tree-rewriting framework resembles Guarded Active XML, a platform handling XML repositories that evolve through web services.