verifying recursive active documents with positive data tree rewriting

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
DOI: 10.4230/lipics.fsttcs.2010.469 Publication Date: 2010-01-01
ABSTRACT
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/>
SUPPLEMENTAL MATERIAL
Coming soon ....
REFERENCES ()
CITATIONS ()
EXTERNAL LINKS
PlumX Metrics
RECOMMENDATIONS
FAIR ASSESSMENT
Coming soon ....
JUPYTER LAB
Coming soon ....