verifying recursive active documents with positive data tree rewriting

• DOI: 10.4230/lipics.fsttcs.2010.469
• Publication Date: 2010-01-01
• Authors: Genest, Blaise; Muscholl, Anca; Wu, Zhilin
• Keywords: FOS: Computer and information sciences; [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB]; well-structured systems.; Other Computer Science (cs.OH); well-structured systems; [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]; Guarded Active XML; Databases (cs.DB); 0102 computer and information sciences; 01 natural sciences; 004; [INFO.INFO-OH] Computer Science [cs]/Other [cs.OH]; Computer Science - Databases; Computer Science - Other Computer Science; tree rewriting; [INFO.INFO-DB] Computer Science [cs]/Databases [cs.DB]; Active documents; data trees; ddc:004; verification

International audience<br/>This paper proposes a data tree-rewriting framework for modeling evolving documents. The framework is close to Guarded Active XML, a platform used for handling XML repositories evolving through web services. We focus on automatic verification of properties of evolving documents that can contain data from an infinite domain. We establish the boundaries of decidability, and show that verification of a {\em positive} fragment that can handle recursive service calls is decidable. We also consider bounded model-checking in our data tree-rewriting framework and show that it is $\nexptime$-complete.<br/>