2026-07-21T14:09:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2887 2024-03-06T10:33:41Z ddc:004 open_access

Verifying Recursive Active Documents with Positive Data Tree Rewriting Genest, Blaise Muscholl, Anca Wu, Zhilin Active documents Guarded Active XML verification data trees tree rewriting well-structured systems. This paper considers a tree-rewriting framework for modeling documents evolving through service calls. We focus on the automatic verification of properties of documents that may contain data from an infinite domain. We establish the boundaries of decidability: while verifying documents with recursive calls is undecidable, we 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. Our data tree-rewriting framework resembles Guarded Active XML, a platform handling XML repositories that evolve through web services. The model here captures the basic features of Guarded Active XML and extends it by node renaming and subtree deletion. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Blaise Genest and Anca Muscholl and Zhilin Wu 2010 Is Part Of LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2010.469 urn:nbn:de:0030-drops-28877 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.469 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode