Verifying Recursive Active Documents with Positive Data Tree Rewriting

Genest, Blaise; Muscholl, Anca; Wu, Zhilin

doi:10.4230/LIPIcs.FSTTCS.2010.469

Document

Verifying Recursive Active Documents with Positive Data Tree Rewriting

Authors Blaise Genest, Anca Muscholl, Zhilin Wu

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2010.469.pdf

Filesize: 0.5 MB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2010.469
URN: urn:nbn:de:0030-drops-28877

Subject Classification

Keywords

Active documents
Guarded Active XML
verification
data trees
tree rewriting
well-structured systems.

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

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.

Cite As Get BibTex

Blaise Genest, Anca Muscholl, and Zhilin Wu. Verifying Recursive Active Documents with Positive Data Tree Rewriting. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 469-480, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.FSTTCS.2010.469

Author Details

Blaise Genest

Anca Muscholl

Zhilin Wu

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail