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
AUTHORS (3)
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 ....