Aspectos de teoría de XPath

SERGIO ABRIOLA

Encuentro; RSME-UMA 2017; 2017

Xpath es el lenguaje de consultas más ampliamente utilizado para documentos XML; es un estándar abierto y constituye una World Wide Web Consortium (W3C) Recommendation. Trabajamos con un fragmento de este lenguaje, apropiadamente reinterpretado como una lógica, en el contexto de árboles con datos y, fundamentalmente, con la capacidad de realizar comparación de datos entre nodos.Desarrollamos la teoría de modelos de XPathd, que solo puede navegar el árbol descendiendo, y XPathv, que tambi\'en puede navegar hacia arriba. Obtenemos resultados de definibilidad y separación para los dos tipos de fórmulas en XPathd: expresiones de nodo y expresiones de camino. También desarrollamos la noción de bisimulación binaria para ambos fragmentos, y demostramos un teorema de caracterización al estilo van Benthem para expresiones de camino de XPathd.Extendemos XPathd al universo de grafos con datos, y analizamos la complejidad computacional de decidir si dos nodos en dos grafos con datos son bisimilares. Calculamos cotas ajustadas de complejidad para varios problemas de bisimilaridad y para diferentes universos de modelos.Introducimos LRV, una lógica para navegar sobre árboles con datos múltiples, y obtenemos procedimientos de decisión para el problema de satisfabilidad de LRV y algunos fragmentos al reducirlo al problema de control-state-reachability de diferentes sistemas con contadores.