Satisfying a Fragment of XQuery by Branching-Time Reduction
Sylvain Hallé, Roger Villemaire · 2008
Configuration Logic (CL) is a fragment of XQuery that allows first-order quantification over node labels. In this paper, we study CL satisfiability and seek a deterministic decision procedure to build models of satisfiable CL formulae. To this end, we show how to revert CL satisfiability into an equivalent CTL satisfiability problem in order to leverage existing model construction algorithms for CTL formulae.