MSc. Research

Satisfiability of XPath Queries with Numerical Constraints

In my Master thesis research, I worked on a more formal aspect of computer science, which is about the investigation of mathematical logics for the optimisation of XPath queries. The emergence of XML as a standard language for structuring and exchanging data has made necessary to optimise the XPath language used to search and retrieve information in XML documents. In this context, I addressed the problem of decidability of XPath queries in order to allow manipulating XML data safely and effectively while significantly reducing the evaluation time of XPath queries. 
 
My work consists in the definition and the static analysis of a logic capable to support the expressive power of XPath queries with counting constraints. I proposed a solution that reduces these queries to PDL (Propositional Dynamic Logic) and u-calculus formulae where models are finite trees. My solution allows to statically analyse and solve the decidability problems (e.g., inclusion, equivalence, join and satisafibility) of XPath queries in a satisfactory amount of time.
 
The main application of my work is a compiler that interprets XPath queries to formulas in the proposed logic in order to decide about them  via the satisfiability solver presented in the works of P. Genevès.