10.4230/LIPICS.FSTTCS.2010.469
Genest, Blaise
Blaise
Genest
Muscholl, Anca
Anca
Muscholl
Wu, Zhilin
Zhilin
Wu
Verifying Recursive Active Documents with Positive Data Tree Rewriting
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2010
Article
Active documents
Guarded Active XML
verification
data trees
tree rewriting
well-structured systems.
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
2010
2010-12-14
2010-12-14
2010-12-14
en
urn:nbn:de:0030-drops-28877
10.4230/LIPIcs.FSTTCS.2010
978-3-939897-23-1
1868-8969
10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS 2010
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
2013
8
40
469
480
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Lodaya, Kamal
Kamal
Lodaya
Mahajan, Meena
Meena
Mahajan
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2010
8
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
526940 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), pages 469-480