Sesión Lógica y ComputabilidadExtensiones expresivas de Propositional Dynamic Logic a través de propiedades topológicas de grafos
Edwin Pin
Universidad de Buenos Aires, Instituto de Ciencias de la Computación, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El sistema formal $\textit{Propositional Dynamic Logic}$ [2], $\text{PDL}$ en adelante, surgió como un lenguaje basado en lógica modal para describir correctitud, terminación y equivalencia de programas. Desde su origen se ha aplicado también con otros propósitos, por ejemplo, como lenguaje de consulta sobre estructuras con forma de grafos [3]. Otro punto importante en el estudio de este lenguaje es lo fácil que se puede adaptar sintácticamente según determinadas necesidades ontológicas a estudiar, como es el caso de [4] donde analizan $\text{ICPDL}$: $\text{PDL}$ + Intersection + Converse. La adhesión de estos nuevos operadores no solo incrementa el poder expresivo de $\text{PDL}$ sino que preservan varias de las propiedades computacionales que $\text{PDL}$ posee.
Más recientemente, en [1] se introdujo el lenguaje $\text{CPDL}^+$ como una extensión de $\text{PDL}$ dotado con un operador nuevo denominado $\textit{programa conjuntivo}$, que es compatible con los demás operadores de $\text{PDL}$ y cuyo propósito es consultar sobre cualquier estructura de Kripke si determinados patrones relativos a grafos con datos surgen en el modelo. Para ello el operador de programa conjuntivo se define junto a la noción de $\textit{grafo subyacente}$ de un programa y bajo este esquema se estudiaron distintos problemas: (1) definición de fragmentos de $\text{CPDL}^+$ mediante propiedades topológicas de grafos, (2) indistinguibilidad de modelos con respecto a fragmentos de $\text{CPDL}^+$ mediante criterios de bisimulación, (3) satisfacibilidad de $\text{CPDL}^+$ y de sus fragmentos, (4) model checking. Los problemas computacionales relacionados a (3) y (4) se demostraron decidibles según el fragmento escogido. Más aún, $\text{CPDL}^+$ es un lenguaje altamente abarcativo, pues contiene a $\text{ICPDL}$, a varias otras extensiones de $\text{PDL}$, y además a algunos lenguajes de interés en el área de bases de datos con forma de grafos, como $\text{C2RPQ}$ [6].
Por lo general, un fragmento de una lógica se obtiene por medio de restricciones sintácticas, pero en el caso de $\text{CPDL}^+$ se pueden definir fragmentos que dependen de características topólogicas impuestas sobre los grafos subyacentes de los programas conjuntivos. En este sentido definimos $\text{CPDL}^+(\mathcal{G})$ como el fragmento de $\text{CPDL}^+$ cuyos programas conjuntivos tienen grafos subyacentes pertenecientes a una clase de grafos $\mathcal{G}$. Una propiedad importante de grafos usada ampliamente en [1] es ``bounded treewidth'', siendo el treewidth de un grafo un parámetro entero que indica qué tan similar es dicho grafo a un árbol [5]. De esta manera, podemos ver a $\text{CPDL}^+$ como la unión de una jerarquía de fragmentos que denotamos $\text{CPDL}^+(\text{TW}_k)$, donde $\text{TW}_k$ es la clase de todos los grafos de treewidth a lo sumo $k$. Bajo esta noción y considerando grafos subyacentes conexos, se demostró que $\text{ICPDL}$ es equiexpresivo a $\text{CPDL}^+(\text{TW}_k)$ para $k = 1, 2$ (i.e. toda fórmula de $\text{ICPDL}$ es equivalente a otra en $\text{CPDL}^+(\text{TW}_k)$ y viceversa). Por otra parte, también se demostró que para todo $k \geq 2$, $\text{CPDL}^+(\text{TW}_k)$ es menos expresivo que $\text{CPDL}^+(\text{TW}_{k+1})$. Para estos fragmentos se estudiaron los problemas especificados en los ítems (2-4). En particular se tienen los siguientes resultados: (2) Para cada $k$, se obtuvo un criterio de indistinguibilidad de modelos para $\text{CPDL}^+(\text{TW}_k)$ en términos de un juego de $k$-piedras, también denominado $k$-$\textit{bisimulación}$. (3) Se demostró que para todo $k$, el problema de satisfacibilidad de $\text{CPDL}^+(\text{TW}_k)$ es decidible en complejidad $\text{2ExpTime}$ , que es igual a la de $\text{ICPDL}$ [4]. (4) El problema de model checking sobre estructuras finitas es polinomial para cualquier $\text{CPDL}^+(\text{TW}_k)$, pero es $\text{NP-hard}$ para $\text{CPDL}^+$.
Trabajo en conjunto con: Diego Figueira (University of Bordeaux, CNRS-LaBRI, France) y Santiago Figueira (Universidad de Buenos Aires, DC, CONICET, ICC).
Referencias
[1] Diego Figueira, Santiago Figueira, and Edwin Pin. PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse. In Annual Symposium on Logic in Computer Science (LICS), Proceedings of Annual Symposium on Logic in Computer Science (LICS), Boston, United States, June 2023.
[2] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194–211, 1979.
[3] Martin Lange. Model checking propositional dynamic logic with all extras. J. Appl. Log., 4(1):39– 49, 2006.
[4] Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. 74(1):279–314, 2009.
[5] Umberto Bertele and Francesco Brioschi. On non-serial dynamic programming. Journal of Combinatorial Theory, Series A, 14(2):137–148, 1973.
[6] Meghyn Bienvenu, Magdalena Ortiz and Mantas Simkus. Conjunctive Regular Path Queries in Lightweight Description Logics. IJCAI '13: Proceedings of the Twenty-Third international joint conference on Artificial Intelligence Pages 761–767, August 2013.