
TL;DR
This thesis develops a fixpoint temporal logic based system for static analysis of XML processing languages, enabling efficient reasoning about XPath and XML schemas with practical applications in static analyzers.
Contribution
Introduces a decidable, expressive logic derived from the mu-calculus for XML analysis, with algorithms and implementation for static type-checking and containment problems.
Findings
Logic is decidable in exponential time.
System effectively handles XPath and XML schema analysis.
Practical experiments show efficiency in realistic scenarios.
Abstract
This thesis describes the theoretical and practical foundations of a system for the static analysis of XML processing languages. The system relies on a fixpoint temporal logic with converse, derived from the mu-calculus, where models are finite trees. This calculus is expressive enough to capture regular tree types along with multi-directional navigation in trees, while having a single exponential time complexity. Specifically the decidability of the logic is proved in time 2^O(n) where n is the size of the input formula. Major XML concepts are linearly translated into the logic: XPath navigation and node selection semantics, and regular tree languages (which include DTDs and XML Schemas). Based on these embeddings, several problems of major importance in XML applications are reduced to satisfiability of the logic. These problems include XPath containment, emptiness, equivalence,…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Semantic Web and Ontologies · Logic, programming, and type systems
