XPath-like Query Logics : Proof Systems and Real-World Applicability - PhDData

Access database of worldwide thesis




XPath-like Query Logics : Proof Systems and Real-World Applicability

The thesis was published by Lick, Anthony, in July 2019, Université Paris-Saclay.

Abstract:

Motivated by applications ranging from XML processing to runtime verificationof programs, many logics on data trees and data streams have been developed in the literature.These offer different trade-offs between expressiveness and computationalcomplexity; their satisfiability problem has often non-elementary complexity or is even undecidable.Moreover, their study through model-theoretic or automata-theoretic approaches can be computationally impractical or lacking modularity.In a first part, we investigate the use of proof systems as a modular way tosolve the satisfiability problem of data logics on linear structures.For each logic we consider, we develop a sound and complete hypersequentcalculus and describe an optimal proof search strategy yielding an NPdecision procedure.In particular, we exhibit an NP-complete fragment of the tense logic over data ordinals—the full logic being undecidable—, which is exactly as expressive as the two-variable fragment of the first-order logic on data ordinals.In a second part, we run an empirical study of the main decidable XPath-likelogics proposed in the literature.We present a benchmark we developed to that end, and examine how these logicscould be extended to capture more real-world queries without impacting thecomplexity of their satisfiability problem.Finally, we discuss the results we gathered from our benchmark, and identifywhich new features should be supported in order to increase the practicalcoverage of these logics.

Motiv√©es par de nombreuses applications allant du traitement XML √† lav√©rification d’ex√©cution de programmes, de nombreuses logiques sur les arbresde donn√©es et les flux de donn√©es ont √©t√© d√©velopp√©es dans la litt√©rature.Celles-ci offrent divers compromis entre expressivit√© et complexit√©algorithmique ; leur probl√®me de satisfiabilit√© a souvent une complexit√© non√©l√©mentaire ou peut m√™me √™tre ind√©cidable.De plus, leur √©tude √† travers des approches de th√©ories des mod√®les ou deth√©orie des automates peuvent √™tre algorithmiquement impraticables ou manquerde modularit√©.Dans une premi√®re partie, nous √©tudions l’utilisation de syst√®mes de preuvecomme un moyen modulaire de r√©soudre le probl√®me de satisfiabilit√© des donn√©es logiques sur des structures lin√©aires.Pour chaque logique consid√©r√©e, nous d√©veloppons un calcul d’hypers√©quentscorrect et complet et d√©crivons une strat√©gie de recherche de preuve optimaledonnant une proc√©dure de d√©cision NP.En particulier, nous pr√©sentons un fragment NP-complet de la logique temporelle sur les ordinaux avec donn√©es, la logique compl√®te √©tant ind√©cidable, qui est exactement aussi expressif que le fragment √† deux variables de la logique du premier ordre sur les ordinaux avec donn√©es.Dans une deuxi√®me partie, nous menons une √©tude empirique des principaleslogiques √† la XPath d√©cidables propos√©es dans la litt√©rature.Nous pr√©sentons un jeu de tests que nous avons d√©velopp√© √† cette fin etexaminons comment ces logiques pourraient √™tre √©tendues pour capturer davantage de requ√™tes du monde r√©el sans affecter la complexit√© de leur probl√®me de satisfiabilit√©.Enfin, nous analysons les r√©sultats que nous avons recueillis √† partir de notre jeu de tests et identifions les nouvelles fonctionnalit√©s √† prendre en charge afin d‚Äôaccro√ģtre la couverture pratique de ces logiques.



Read the last PhD tips