Publication
We present an algorithm to solve XPath decision problems under regular tree type constraints and show its use to statically type-check XPath queries. To this end, we prove the decidability of a logic with converse for finite ordered trees whose time complexity is a simple exponential of the size of a formula. The logic corresponds to the alternation free modal mu-calculus without greatest fixpoint, restricted to finite trees, and where formulas are cycle-free.
Mikhail Kapralov, Jakab Tardos, Navid Nouri, Aidasadat Mousavifar
Serge Vaudenay, Fatma Betül Durak
François Fleuret, Angelos Katharopoulos, Apoorv Vyas