文章基本信息

标题：Verifying Recursive Active Documents with Positive Data Tree Rewriting
本地全文：下载
作者：Blaise Genest ; Anca Muscholl ; Zhilin Wu 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2010
卷号：8
页码：469-480
DOI：10.4230/LIPIcs.FSTTCS.2010.469
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Active documents; Guarded Active XML; verification; data trees; tree rewriting; well-structured systems.