Análisis de complejidad de lógicas temporales

Análisis de complejidad de lógicas temporales Complexity analysis of temporal logics Trabajo de Fin de Grado Curso 2023–2024 Autor Sergio Javier Hernando Rivero Directores Ismael Rodríguez Laguna Natalia López Barquilla Doble grado en Ingeniería Informática y Matemáticas Facultad de Informática Universidad Complutense de Madrid Análisis de complejidad de lógicas temporales Complexity analysis of temporal logics Trabajo de Fin de Grado de Doble Grado Ingeniería Informática y Matemáticas Autor Sergio Javier Hernando Rivero Directores Ismael Rodríguez Laguna Natalia López Barquilla Convocatoria: Junio 2024 Doble grado en Ingeniería Informática y Matemáticas Facultad de Informática Universidad Complutense de Madrid 27 de Mayo de 2024 Agradecimientos En primer lugar, quiero agradecer a mis tutores y directores de trabajo de fin de grado, Natalia López Barquilla e Ismael Rodríguez Laguna, por brindarme apoyo, paciencia y experiencia a lo largo de todo el proceso. Además, les agradezco haberme propuesto un tema tan interesante y haberme provisto de bibliografía para comenzar el trabajo. Agradezco también a mi hermano Alejandro y a mis compañeros Jaime, Gonzalo y Amaia por sus consejos a la hora de escribir y refinar mis argumentos, así como su ayuda a la hora de corregir erratas en el propio trabajo. Finalmente, extiendo mi gratitud a todo el mundo que, de una forma u otra, ha contribuido en algún momento del desarrollo de este trabajo. v Resumen Análisis de complejidad de lógicas temporales En este Trabajo de Fin de Grado (TFG) se lleva a cabo un estudio de la complejidad computacional de la satisfacibilidad de lógicas temporales. En particular, se analiza la complejidad de contar el número de interpretaciones que hacen cierta una fórmula en LT L oLT L⋄, dos lógicas temporales lineales. El objetivo principal de este trabajo es utilizar resultados conocidos para la lógica LT L y deducir resultados innovadores sobre LT L⋄utilizándolos. Además, este documento ofrece un acercamiento a las lógicas temporales y a las clases de complejidad, especialmente a las clases de complejidad de conteo. En el desarrollo de este trabajo se distinguen tres tipos de interpretaciones sobre los cuales el problema de la satisfacibilidad es determinista. Estas valoraciones temporales son las palabras periódicas, los k-árboles y los k-grafos. El análisis formal de complejidad de conteo se realiza considerando cada uno de estos modelos de forma independiente. Los resultados obtenidos reflejan una similitud entre la complejidad de contar modelos de palabras periódicas y k-grafos, debido a que estos modelos tienen un tamaño similar. Por otro lado, se observa una mayor complejidad en los k-árboles en relación a los otros dos tipos de modelos, ya que los k-árboles tienen una cantidad de nodos exponencialmente mayor. En resumen, este trabajo ofrece una visión integral sobre la complejidad de conteo en lógicas temporales lineales, proporcionando resultados significativos y estableciendo una base para futuras investigaciones en el análisis de LT L⋄. Palabras clave Complejidad computacional, Lógica temporal, LT L,LT L⋄, Problemas de conteo, Model Counting, #P-completitud, #PSPACE-completitud. vii Abstract Complexity analysis of temporal logics In this Final Degree Project, we conduct an in-depth analysis of computational complexity of satisfiability of temporal logics. In particular, we analyse the computational complexity of counting the number of interpretations which satisfy an instance of LT L or LT L⋄, two lineal-time temporal logics. The main objective of this project is the use of known results in LT L complexity to deduce and prove new results for LT L⋄. Additionally, this document offers an approach to temporal logics and complexity classes, in particular counting complexity classes. In this project, three types of models are defined: periodic words, k-trees and kgraphs. These models are chosen because determining satisfiability in each of these models is deterministic. This study offers an independent analysis of the counting computational complexity of determining how many of each of these models satisfy a certain formula. The results obtained show a similarity between counting periodic word models and k-graph models, mainly due to the similar size of these models. However, a significant difference is observed when analysing k-trees, exponentially larger that the two prior models. Overall, this project offers a general perspective over the counting complexity in linear-time temporal logic. It also helps provide significant results in LT L⋄analysis and acts as a stepping stone for future research in the topic. Keywords Computational complexity, Temporal logic, LT L,LT L⋄, Counting problems, Model Counting, #P-completeness, #PSPACE-completeness ix 2Capítulo 1. Introducción 1.2. Objetivos de la investigación El objetivo de este Trabajo de Fin de Grado es analizar la complejidad de contar modelos que satisfacen una fórmula de LT L y utilizar esos resultados para resolver problemas análogos empleando fórmulas de LT L⋄, una lógica temporal estrictamente contenida en LT L. Otro objetivo es el acercamiento y familiarización con lógicas temporales y los razonamientos de complejidad, en particular los relacionados con la complejidad de conteo. 1.3. Plan de trabajo Este trabajo se ha realizado en dos fases: 1. Investigación: Durante la fase de investigación se estudió en primer lugar documentación sobre clases de complejidad de conteo, comenzando por el capítulo 17 de Arora y Barak (2006), por recomendación de los tutores. A raíz de eso, se buscó información sobre razonamientos espacio-temporales, con la intención de formalizar el problema de determinar el número de pasados probables para situaciones presentes dadas. Una vez hecho esto, el objetivo era analizar la complejidad del problema de la determinación de pasados factibles en casos aplicados. Tras una reunión con los tutores, se tomó la decisión de generalizar este enfoque y analizar la complejidad de lógicas temporales. Así, se buscaron artículos relacionados con la complejidad de problemas de conteo en lógicas temporales. Al haber encontrado, leído y comprendido el artículo Torfah y Zimmermann (2014), se decidió investigar la complejidad de contar las soluciones a fórmulas en LT L⋄. 2. Desarrollo: Una vez se hubo concretado el objetivo de la investigación, se utilizaron los resultados obtenidos por otros autores en complejidad de conteo de modelos en fórmulas de LT L para deducir y demostrar nuevos resultados sobre la complejidad del problema de contar el número de modelos de fórmulas en LT L⋄. En particular, se distinguieron tres tipos de modelos distintos en los que la satisfacibilidad es determinista y se realizó un análisis de la complejidad de contar el número de cada uno de los tipos de modelos que satisfacen una fórmula en LT L⋄. 1.4. Estructura del trabajo 3 1.4. Estructura del trabajo El resto de este trabajo está dividido en 5 capítulos, siguiendo la estructura que se presenta a continuación: 1. El capítulo 2 actúa como preámbulo, introduciendo algunos conceptos necesarios para comprender la estructura y resultados que se presentan en el siguiente capítulo. Se definen clases de complejidad relevantes (así como una jerarquía entre las mismas) y las distintas lógicas sobre las cuales se investigará. 2. En el capítulo 3 se encuentra el grueso de este Trabajo de Fin de Grado. En este se presenta el trabajo realizado por el autor y los resultados que se han demostrado, así como resultados similares de otros autores. 3. El capítulo 4 ofrece una breve recopilación de los resultados del capítulo anterior, un análisis de los mismos y posibilidades de trabajo futuro. 4. Por último, los capítulos 5 y 6 están formados por traducciones al inglés de los capítulos 1 y 4, respectivamente. Cap´ ıtulo 2 Contexto de la investigación Para realizar razonamientos lógicos sobre situaciones físicas, es necesario un lenguaje lo suficientemente expresivo. Este debe ser capaz de formalizar adecuadamente todos los enunciados que necesitamos. La lógica más utilizada en matemáticas es la lógica de primer orden. Esta lógica es una combinación de lógica de predicados y cuantificadores. No obstante, para realizar razonamientos lógicos sobre conjuntos sencillos se emplea una lógica conocida como lógica proposicional. Esta es una lógica más sencilla que la lógica de primer orden y que utiliza símbolos de proposición que representan ideas atómicas y no incluye cuantificadores. Una lógica proposicional está formada por dos conjuntos PyO, donde el primer conjunto es llamado conjunto de símbolos de proposición y el segundo se denomina conjunto de operadores. Se tiene además que existe una función ar:O → N, tal que si ar(o) = nse dice que oes un operador n-ario. Consideraremos que el conjunto Ocontiene los siguientes operadores: 1. ¬: operador unario de negación, es decir, invierte el valor de verdad de la afirmación que lo sucede. 2. ∨: operador binario que representa el or lógico. 3. ∧: operador binario que representa el and lógico. 4. ⊥y⊤: operadores sin argumentos que representan la falsedad y la certeza, respectivamente. Dado un conjunto de símbolos de proposición Py los operadores de O, se pueden definir formalmente las fórmulas del lenguaje LPsiguiendo las siguientes reglas de formación: 1. ⊤y⊥ ∈ LP 2. ∀p∈ P,p∈LP 3. Si φ∈LP,¬φ∈LP 5 6Capítulo 2. Contexto de la investigación 4. Si φ1, φ2∈LP, (φ1∗φ2)∈LP,donde ∗ ∈ {∧,∨} Los paréntesis en la fórmula anterior actúan como complemento sintáctico a PyO. Habiendo determinado la sintaxis de la lógica proposicional, surge la idea natural de determinar si algo expresado mediante estas fórmulas puede ser cierto o no. Este problema es exactamente SAT, el problema de satisfacibilidad booleana de una fórmula dada. Para llevar acabo la determinación de verdad de una fórmula, es necesario asignar un valor (cierto o falso) a cada símbolo de proposición de Py calcular el valor de verdad de las fórmulas usando la semántica específica de cada operador. Definición 2.0.1. Una valoración ves una función v:P −→ {0,1}que hace corresponder a cada símbolo de proposición un valor de verdad. Se denota ⊥una fórmula que es siempre falsa y ⊤una fórmula siempre cierta. Definición 2.0.2. Dado un conjunto Pde símbolos de proposición, φ∈LPuna fórmula y una valoración v:P −→ {0,1}, definimos el valor de verdad de φcon v y lo denotamos por φvpor recursión estructural: 1. Sea φ∈ P,φv=v(φ),⊥v= 0 y⊤v= 1 2. φ=¬φ′,φv=(0si φ′v= 1 1si φ′v= 0 3. φ=φ1∧φ2,φv=v∧(φv 1, φv 2), donde v∧(φv 1, φv 2) = (1si φv 1=φv 2= 1 0si φv 1= 0 oφv 2= 0 4. φ=φ1∨φ2, φv=v∨(φv 1, φv 2), donde v∨(φv 1, φv 2) = (1si φv 1= 1 oφv 2= 1 0si φv 1=φv 2= 0 La satisfacibilidad booleana de una fórmula φse cumple cuando existe alguna valoración vtal que φv= 1. El hecho de que vsea una valoración que satisface φse denota por v|=φy se dice que ves modelo de φ. A partir de la satisfacibilidad de una fórmula podemos definir la satisfacibilidad de un conjunto de fórmulas Φ⊆LP, que se tiene cuando una valoración vsatisface todas las fórmulas contenidas en Φ. Esto también se denota por v|= Φ. Finalmente, si cualquier valoración vtal que v|= Φ cumple que para una cierta fórmula φ,v|=φ, decimos que φes consecuencia lógica de Φy lo denotamos por Φ|=φ. 2.1. La lógica LT L o linear-time temporal logic Existen extensiones de la lógica proposicional que incluyen otros operadores, cuyo objetivo es proporcionar una mayor expresividad. Para definir expresiones relativas 2.1. La lógica LT L o linear-time temporal logic 7 al tiempo, podemos añadir al lenguaje de lógica proposicional un nuevo parámetro, T. Este parámetro representa el tiempo mediante un conjunto infinito totalmente ordenado. Esto quiere decir que, dados dos elementos t1, t2∈ T ,t1< t2implica que t1sucede antes que t2y que ∀t1, t2∈ T se tiene t1< t2,t1> t2ot1=t2, por lo que no hay ramificaciones en el tiempo. Con esta noción en mente podemos definir la lógica LT L (linear-time temporal logic) como una tupla de tres elementos (P, O,T), cuyos operadores son los definidos anteriormente para la lógica proposicional más los siguientes: 1. Operador until (binario): φ1Uφ2indica que existe un punto donde se cumple la propiedad φ2y la propiedad φ1se cumple siempre por lo menos hasta ese punto. 2. Operador release (binario): φ1Rφ2indica que φ2es cierto hasta el primer momento en el que φ1lo es. En caso de que esto no ocurra, φ2debe ser cierto siempre 3. Operador next (unario): Xφque indica que, denotando por tel instante actual, la proposición se cumple en el instante t+ 1. La lógica LT L es un subconjunto de la lógica de primer orden que incluye estrictamente a la lógica proposicional. En ella, no todos los operadores aportan expresividad, porque UyRson igualmente expresivos. De hecho, el operador Rpuede ser expresado en términos del operador Umediante la construcción φ1Rφ2=¬(¬φ1Uφ2). Al haber añadido estos tres operadores se obtiene una lógica mucho más expresiva que la lógica proposicional. A partir de los operadores proposicionales y los que acabamos de definir se pueden establecer operadores como los operadores unarios ⋄ (en algún momento) o □(siempre en el futuro). El operador ⋄es expresable con el operador Umediante la construcción ⋄φ=⊤Uφy el operador □es deducible a partir del operador ⋄mediante la construcción □φ=¬⋄¬φ. De la misma manera, el operador ⋄se puede expresar de forma análoga en términos de □mediante la construcción ⋄φ=¬□¬φ. Las reglas de formación sintácticas de LT L son las siguientes: 1. ∀φ∈LP, φ ∈ LT L. 2. Si φ∈ LT L,&φ∈ LT L donde &∈ {X,⋄,□} 3. Si φ1, φ2∈ LT L, (φ1∗φ2)∈ LT L,donde ∗ ∈ {U,R} Con estos operadores en mente, se define la lógica LT L⋄, que añade únicamente los operadores ⋄y□anteriormente definidos a la lógica proposicional usual. Este tipo de construcciones que emplean subconjuntos de LT L serán objeto de estudio más adelante. La sintaxis operacional de LT L⋄es análoga a la de LT L eliminando las construcciones que emplean X,UyR. 8Capítulo 2. Contexto de la investigación No obstante, no estamos en condiciones de hacer razonamientos en esta lógica, ya que solo disponemos de herramientas para formalizar expresiones. Es decir, no tenemos una semántica. Para ello necesitamos introducir el concepto de valoración temporal o interpretación. Definición 2.1.1. Una valoración temporal o interpretación es una función π:T → 2|P| que asigna a cada instante ten Tel conjunto de las proposiciones atómicas que son ciertas en t. Se tiene por tanto π(t)|=φcuando la valoración vinducida por la evaluación de πen el instante tcumple v|=φ. La aplicación de πsobre cualquier expresión en LT L se define por inducción estructural. Sea tun instante de tiempo cualquiera: 1. π(t)|=⊥yπ(t)|=⊤. 2. π(t)|=ppara p∈ P si p∈π(t). 3. π(t)|=¬φsi π(t)|=φ. 4. π(t)|=φ1∧φ2si π(t)|=φ1yπ(t)|=φ2. 5. π(t)|=φ1∨φ2si π(t)|=φ1oπ(t)|=φ2. 6. π(t)|=Xφsi π(t+ 1) |=φ. 7. π(t)|=φ1Uφ2si ∃t1≥ttal que π(t1)|=φ2y∀t2∈[t, t1]se tiene π(t2)|=φ1. 8. π(t)|=φ1Rφ2(si ∀t1≥t, π(t1)|=φ2yπ(t1)|=φ1 o∃t2> t, π(t2)|=φ1yπ(t2)|=φ2. 9. π(t)|=⋄φsi ∃t1> t tal que π(t1)|=φ. 10. π(t)|=□φsi ∀t1≥tse cumple π(t1)|=φ. De la misma manera que hemos definido la sintaxis de LT L⋄como una restricción de la de LT L, definimos su semántica como una restricción de la anterior que elimina las cláusulas 6, 7 y 8 de la anterior lista. Mediante una analogía con la sección anterior, decimos que una valoración temporal es un modelo de un conjunto de fórmulas Φ, denotado por π(t)|= Φ, si para cada φ∈Φ,π(t)|=φ. Si para cada valoración π(t)tal que π(t)|= Φ se cumple π(t)|=φpara una cierta fórmula φ∈ LT L, decimos que φes consecuencia lógica de Φ, denotado por Φ|=φ. Además, denotaremos a partir de este momento π|=φsi y solo si ∀t, π(t)|=φ. Habiendo definido las semánticas de las tres lógicas que nos interesan (LP,LT L yLT L⋄), tenemos reglas que permiten inferir si una valoración es modelo o no de una fórmula. El objetivo de este TFG es analizar la complejidad de una variante del problema (que se definirá más adelante) de satisfacibilidad bajo distintas condiciones. Para ello es necesario definir la noción de clase de complejidad, así como introducir una serie de clases que aparecerán más adelante. 2.2. Clases de complejidad 9 2.2. Clases de complejidad En complejidad computacional, se dice que una clase de complejidad es un conjunto de problemas que son similarmente complejos. Esta similitud se mide con su rendimiento en algún parámetro, habitualmente tiempo de computación o espacio en memoria. 2.2.1. La clase de complejidad P La clase de complejidad Pestá definida de forma explícita por los lenguajes que la forman. Definimos un lenguaje formal L⊆ {0,1}∗como un conjunto de palabras contenidas en {0,1}∗. A partir de un lenguaje formal se puede definir el problema de decisión asociado a ese lenguaje Ldeterminando si una palabra cualquiera w∈ {0,1}∗está contenida en L. Decimos que este problema está en la clase de complejidad Psi y solo si existe una máquina de Turing determinista que lo decida en un tiempo menor que P(n), donde P(n)es un polinomio de orden finito. Se dice que un problema contenido en esta clase es polinómico. El parámetro nse corresponde con el tamaño de la entrada proporcionada a la máquina. Un ejemplo de un problema en Pes la búsqueda de un elemento en una lista de nelementos, que, suponiendo que leer y comparar un elemento tiene un coste en tiempo constante menor o igual a una cierta constante c, consiste simplemente en recorrer la cinta de la máquina de Turing hasta encontrarlo. En caso de terminar la cinta y no haber encontrado el elemento, sabemos que no está, por lo que el problema es decidible. En este caso particular, el tiempo tardado es menor o igual a c·n. Se conocen una gran cantidad de problemas en la clase P, y se suele considerar que los problemas en esta clase son computacionalmente asequibles, ya que para valores de nsuficientemente grandes, cualquier programa con un tiempo de ejecución mayor que todo polinomio resulta impracticable. De la misma manera, se dice que los problemas que se ejecutan en tiempo polinómico son tratables o "fácilmente computables". Esta hipótesis se denomina tesis de Cobham, cuyos detalles pueden ser consultados en Cobham (1965). Además, Pes una clase razonable e intuitiva desde el punto de vista de un programador, ya que cualquier subrutina eficiente que un programador diseña se ejecuta en tiempo lineal, cuadrático o alguna combinación de funciones con un tiempo de ejecución polinómico de exponente bajo. En general, si esas subrutinas se llaman desde programas eficientes, obtenemos así composiciones arbitrarias de polinomios, cuyos costes definen la clase P. 2.2.2. La clase de complejidad NP Esta clase de complejidad se corresponde con la noción intuitiva de ser eficientemente verificable, es decir, existe una máquina de Turing que determina si una solución puede ser verificada en tiempo polinómico. Esto implica que la longitud 10 Capítulo 2. Contexto de la investigación de dichas soluciones no puede ser demasiado grande, como mucho polinómica en la longitud de la entrada. A la hora de definir formalmente esta noción definimos la clase NP por los lenguajes L⊆ {0,1}∗para los cuales existe un polinomio p:N→Ny una máquina de Turing Mtal que para cada x∈ {0,1}∗se tiene x∈L⇐⇒ ∃u∈ {0,1}p(|x|)tal que M(x, u) = 1 donde |x|es la longitud de la palabra x. En este caso se dice que ues un certificado para xrespecto al lenguaje Ly la máquina M. Es evidente que P ⊆NP, ya que si algo es computable en tiempo polinómico su resultado se puede utilizar como verificación. Se desconoce si P =NP, problema inmortalizado en los Problemas del Milenio de la Clay Foundation. 2.2.3. NP-completitud Decimos que un lenguaje L⊆ {0,1}∗es reducible en tiempo polinómico a otro lenguaje L′⊆ {0,1}∗, denotado como L≤pL′, si existe una función fcomputable en tiempo polinómico tal que para cada x∈ {0,1}∗,x∈L⇐⇒ f(x)∈L′. De esta manera decimos que un problema L′es NP-duro si L≤pL′∀L∈NP. De la misma manera, los problemas NP-completos son aquellos que son NP-duros y están contenidos en la propia clase NP. Un caso de reducciones particularmente interesante es el de las reducciones parsimónicas, que preservan el número de soluciones de ambos problemas. Informalmente, actúan como una biyección entre las soluciones de AyB. Formalmente, dada una instancia xdel problema A, una reducción es parsimónica si el número de soluciones, o certificados, de xes igual al número de soluciones de f(x), instancia del problema B. 2.2.4. Las clases PSPACE y NPSPACE De la misma manera que se han definido las clases de complejidad P y NP como las clases cuyos problemas se pueden resolver y verificar en tiempo polinómico, respectivamente, surge la idea de definir clases cuyos problemas se pueden resolver o verificar empleando un espacio polinómico con el tamaño de la entrada. La definición formal de ambas clases pasa por considerar las ya ofrecidas anteriormente con la excepción de cambiar la idea de tiempo o número de operaciones por la de espacio en memoria o tamaño de la cinta de la máquina de Turing. Definimos así la clase PSPACE como el conjunto de los problemas de decisión que pueden 2.3. Los problemas de conteo y la clase de complejidad #P 11 ser resueltos por una máquina de Turing determinista en espacio p(n)y tiempo ilimitado, donde pes un polinomio en función de n, el tamaño de la entrada. Además, podemos definir la clase NPSPACE como el conjunto análogo a PSPACE con una máquina de Turing no determinista. Entre las clases presentadas anteriormente se establecen las siguientes relaciones: P⊆NP ⊆PSPACE =NPSPACE La igualdad entre las dos últimas clases viene dada por el teorema de Savitch, consultable en Savitch (1970). 2.2.5. Otras clases de complejidad También definiremos las clases EXPTIME, EXPSPACE y 2EXPSPACE para entradas de tamaño n. EXPTIME es la clase de complejidad que comprende los problemas de decisión que pueden ser resueltos por una máquina de Turing determinista utilizando una cantidad de tiempo exponencial (en O(2p(n))). EXPSPACE, por otro lado, se refiere a la clase de problemas de decisión resueltos por una máquina de Turing determinista en una cantidad de espacio en O(2p(n)). Finalmente, 2EXPTIME denota la clase de problemas de decisión que pueden ser resueltos por una máquina de Turing determinista en un tiempo en O(22p(n)). 2.3. Los problemas de conteo y la clase de complejidad #P Hasta este momento se han mencionado únicamente clases de problemas de decisión (cuya solución es binaria y booleana) y las jerarquías entre ellas. En muchas ocasiones, sin embargo, nos interesa contar el número de certificados que resuelven el problema. Esto es fundamental en numerosas áreas, destacando entre ellas el cálculo de probabilidades. Efectivamente, para poder determinar la probabilidad de un suceso es necesario calcular el número de soluciones que tiene un problema, por lo que el análisis computacional del número de soluciones nos proporciona un análisis de la complejidad de esta tarea. De esta manera, un problema de conteo recibe la misma entrada que un problema de decisión, pero su salida es un número natural que indica el número de posibles soluciones distintas a esa determinada instancia. Como ejemplo canónico de esta clase de problemas se emplea #SAT, la versión de conteo del problema de satisfacibilidad booleana. Dada una fórmula proposicional booleana φ, #SAT consiste en analizar el número de valoraciones distintas que se pueden dar a los símbolos de proposición de φque satisfacen φ. Para analizar la complejidad de los problemas de conteo se definen clases de complejidad propias. La más empleada es la clase de complejidad #P, sharp-P o count-P, 18 Capítulo 3. Complejidad de distintos modelos de lógica temporal Estudiaremos entonces distintas dependencias basadas en letras. Definición 3.0.1. Una letra es un conjunto de símbolos de proposición que son ciertos en un instante dado. Estas letras son exactamente la evaluación π(t)de una valoración temporal πen un instante t, pero son denominadas letras para simplificar y justificar la notación en los tres tipos de valoraciones temporales que emplearemos en este capítulo: palabras periódicas, k-árboles y k-grafos. De nuevo para simplificar notación y por analogía con la teoría de grafos, estas letras también son conocidas como nodos en el estudio de k-árboles y k-grafos. En consecuencia, la acción de la aplicación πen el instante t, definida en 2.1.1, es asignar la letra que corresponde a dicho momento y, con ello, determinar qué proposiciones atómicas son ciertas en ese instante. 3.1. Cadenas acotadas Hemos observado que no todas las valoraciones temporales son igualmente útiles a la hora de determinar si son modelo o no de una determinada fórmula. Por lo tanto, nos interesa considerar sólo interpretaciones para las que podamos afirmar de forma finita y determinista si son o no modelo de una fórmula. Autores en este campo, en particular Torfah y Zimmermann (2014), emplean tres tipos de interpretación distinta con este propósito. Estas valoraciones temporales deben tener suficientes regularidades como para poder determinar de forma precisa la veracidad de fórmulas y trabajan con conjuntos Tnumerables. Estos modelos son las palabras periódicas, los k-árboles y los k-grafos. Como breve recordatorio, decimos que una interpretación πes modelo de una fórmula φcuando se tiene π(t)|=φ ∀t∈ T . Por ejemplo, para la fórmula φ=□p(siempre se cumple p) y T=N, las interpretaciones π1(t) = {p}yπ2(t) = {p, q} ∀t∈ T son dos modelos de φ, mientras que la interpretación π3(1) = {p}, con π3(t) = {q} ∀t∈ T ;t= 1 no es modelo, ya que ∃t0= 2 tal que π(t0)|=φ. Cabe destacar que los tipos de interpretación que se mencionan más adelante, los que se analizan en Torfah y Zimmermann (2014), no son las únicas interpretaciones que dan lugar a modelos. En el artículo Sistla y Clarke (1985), primer acercamiento al análisis de complejidad computacional de lógicas temporales, se emplean únicamente interpretaciones abstractas similares a las palabras periódicas. Sin embargo, este trabajo estudiará tres tipos de interpretaciones de cadenas acotadas, por considerarlos más generales y diversos. 3.1. Cadenas acotadas 19 3.1.1. Valoraciones temporales basadas en palabras periódicas En la definición 3.0.1 se ha definido lo que es una letra, un conjunto de proposiciones atómicas ciertas en un instante concreto. Decimos entonces que una palabra de tamaño kes un conjunto ordenado de letras formado por dos secuencias de letras uyvformadas, a su vez, por secuencias cualesquiera de letras tal que el número de letras total sume k. Es decir, tales que |u|+|v|=k, donde kes una cierta cota dada de antemano. Además, la secuencia vse repite arbitrariamente. Decimos que ues el prefijo y vel periodo de la palabra uv(v∗), donde el asterisco indica que vse puede repetir una cantidad arbitraria de veces (incluso ninguna), representando todas ellas la misma valoración temporal. Este significado del asterisco es exactamente el usado habitualmente en la definición de expresiones regulares. Para abreviar, denotaremos la palabra uv(v∗)definida por las dos secuencias uy vescribiendo uv. Cada letra en la secuencia representa una valoración temporal en un instante de tiempo y la transición de una letra a otra se produce en cada instante, de ahí que necesitemos que el conjunto Tsea numerable para este tipo de modelos. Como ejemplo de interpretaciones basadas en palabras periódicas se muestran valoraciones temporales aplicadas a la fórmula φ=□(p∨(q−→ X r)). En la figura 3.1 se observa un modelo de longitud 3, en la figura 3.2 uno de longitud 2 y en la figura 3.3 una interpretación que no es modelo de φ. Figura 3.1: Modelo de longitud 3 Figura 3.2: Modelo de longitud 2 Figura 3.3: Interpretación temporal no modelo de φ 20 Capítulo 3. Complejidad de distintos modelos de lógica temporal 3.1.2. Valoraciones temporales basadas en k-árboles Los dos siguientes tipos de interpretación están menos basados en los lenguajes regulares y más en la teoría de grafos. El primer tipo de valoraciones temporales está basado en la noción de árbol dirigido que se emplea habitualmente en teoría de grafos. De esta manera, las valoraciones en cada instante son llamadas nodos. Una valoración temporal basada en un k-árbol es una interpretación cuyo comportamiento se puede modelizar mediante un grafo similar a un árbol dirigido de altura k, donde el estado inicial (la valoración en el primer instante de tiempo) es el nodo raíz y cuya anchura por número de hijos es una constante cdeterminada. Estas interpretaciones no son exactamente árboles, ya que además, de cada nodo hoja, parte una arista hacia algún nodo en la misma rama. De esta manera, cada rama es una palabra periódica. Cada árbol define más de una interpretación π, ya que la letra correspondiente al instante t+ 1 corresponde a uno cualquiera de los hijos de la letra en el instante t, salvo que esta sea una hoja (en cuyo caso la letra siguiente es determinista). De hecho, infinitas valoraciones temporales distintas pueden tener un mismo kárbol asociado. Decimos que un k-árbol Aes modelo de una fórmula cuando todas las interpretaciones cuyo k-árbol asociado es un subgrafo de Ason modelo de dicha fórmula. El problema que nos interesa en este caso es contar el número de k-árboles diferentes que son modelo de una cierta fórmula. A continuación se muestra en la figura 3.4 un 2-árbol modelo de la fórmula φ=□(p∨(q−→ X r)). Figura 3.4: Modelo de 2-árbol de φ 3.1.3. Valoraciones temporales basadas en k-grafos El último tipo de valoraciones temporales que este trabajo estudiará son las valoraciones basadas en k-grafos. Una valoración temporal basada en un k-grafo es una interpretación cuyo comportamiento se puede modelizar como un sistema de transiciones dirigidas de k estados, un grafo dirigido donde cada estado es alcanzable desde el inicial, evitando así estados inalcanzables y donde cada estado puede tener varias aristas salientes, 3.2. Model Counting 21 incluyendo autoaristas. Ocurre en estos modelos un fenómeno similar al que se observa en los k-árboles, ya que cada transición en un nodo con varias aristas salientes da lugar a ese número de interpretaciones distintas. De nuevo, nos interesará contar los k-grafos en los cuales todas las interpretaciones son modelo de la fórmula que nos interese. En la figura 3.5 se muestra un ejemplo de 4-grafo modelo de la fórmula LT L □(p∨(q−→ X r)) que se mostró anteriormente. Figura 3.5: Modelo de 4-grafo de φ 3.2. Model Counting El problema que nos interesa, a diferencia del enfoque de decisión, más frecuente y preocupado por la existencia de una única valoración temporal que sea modelo de una fórmula, es contar el número de palabras periódicas, k-árboles o k-grafos que satisfacen una determinada fórmula. Este problema es equivalente, en el caso general, a la búsqueda de interpretaciones que son modelo de una fórmula, indecidible en muchos casos. Precisamente por esto se han definido los modelos anteriores, diferenciando casos más o menos complicados. A lo largo de esta sección, las demostraciones sobre la complejidad de LT L presentadas se pueden consultar en Torfah y Zimmermann (2014). Se muestran algunas por su utilidad para desarrollar argumentos propios y otras por proporcionar un contexto completo. Todas las demostraciones que hacen referencia a LT L⋄son originales de este trabajo. 3.2.1. Model counting para modelos de palabras periódicas Habiendo definido el problema que nos interesa analizar, model counting, particularizaremos este para contar las palabras periódicas de longitud kque son modelo de una cierta fórmula en una lógica temporal. 22 Capítulo 3. Complejidad de distintos modelos de lógica temporal Comenzaremos analizando el caso en el que kes un número dado en unario, donde la representación de ktoma exactamente ese número de símbolos en la máquina de Turing. Esto contrasta con el caso en el que kestá codificado en binario. Aquí, la representación de ken la cinta de la máquina de Turing emplea log2(k)símbolos. Formalmente corresponde con el problema: Dadas una fórmula de LT L φy una cota (escrita en unario), ¿cuantas palabras periódicas de longitud kmodelan φ? Teorema 3.2.1. Model counting para cadenas periódicas acotadas con k unario pertenece a #P. Demostración. Para ver que está en #P definimos una máquina de Turing no determinista Mde la siguiente manera. La máquina adivina un prefijo uy un periodo vde una palabra periódica, con |uv|=ky comprueba de forma determinista en tiempo polinómico si uv modela φ. Por lo tanto, cada ejecución define únicamente una palabra y encontrar todos los modelos se puede realizar contando las ejecuciones en las que Macepta. Tenemos además que este problema es una generalización de #SAT, ya que si fijamos k= 1 y una fórmula φ∈LPobtenemos un caso particular de Model counting para LT L yLT L⋄que se corresponde exactamente con #SAT. Como #SAT es un problema #P-duro, cualquier generalización del mismo lo es también. Dado que la representación en unario de 1es idéntica a su representación en binario, este resultado se tiene en ambos casos. Corolario 3.2.1.1. Model counting para cadenas periódicas acotadas con k unario es #P-completo. Si consideramos que la cota kestá escrita en binario, el problema cambia. Estaríamos contestando entonces al problema análogo: Dadas una fórmula de LT L φy una cota (escrita en binario), ¿cuántas palabras periódicas de longitud kmodelan φ? Este problema es #PSPACE-completo. Para verlo comenzaremos demostrando que está en #PSPACE. Teorema 3.2.2. Model counting para cadenas periódicas acotadas con kbinario pertenece a #PSPACE. Demostración. No podemos simplemente adivinar una palabra de longitud kporque está codificado en binario (y el tamaño de esa palabra es exponencial respecto al tamaño de la entrada). Construimos entonces nuestra máquina de Turing que adivina una palabra representada por uv adivinando u$v, donde $ es un símbolo que indica el comienzo del periodo. De esta manera, la palabra u$vse puede escribir como w(0)...w(i− 1)$w(i)...w(k−1), donde w(i)indica la letra i-ésima de la palabra uv. El símbolo 3.2. Model Counting 23 $ es útil únicamente para denotar el comienzo del periodo. Para cumplir con los requisitos de espacio, la máquina Msolo almacena el símbolo w(j)para cada instante de tiempo j∈ T , descarta símbolos adivinados anteriormente y lleva un contador para adivinar exactamente ksímbolos. Para verificar que uv |=φ,Mcrea para cada jen el rango 0≤j < k un conjunto Cjde subfórmulas de φcon la intención de que Cjcontenga exactamente las subfórmulas que se satisfacen en la posición jde uv. De nuevo, no podemos almacenar todos los conjuntos, así que se almacenan tres conjuntos: Cj,Cj+1 y Ck−1. El último es adivinado por My los conjuntos j < k −1se determinan de forma unívoca por las reglas siguientes: 1. La pertenencia a Cjde proposiciones atómicas es determinado por w(j), porque este es una letra. 2. Las conjunciones, disyunciones y negaciones se comprueban localmente. Por ejemplo, ¬p∈Cjsii p /∈Cj. 3. Las fórmulas Xse propagan hacia atrás usando la equivalencia: Xφ∈Cjsii φ∈Cj+1. 4. Las fórmulas que contienen Uutilizan la equivalencia: φ0Uφ1∈Cjsi y solo si se da φ1∈Cjo se da φ0∈Cjyφ0Uφ1∈Cj+1. 5. El resto de operadores se pueden reescribir en términos de los anteriores (incluyendo R). Una vez Mha adivinado el periodo al completo, comprueba que el conjunto Ck−1 es correcto. Esto ocurre si se verifican los requisitos: 1. Para cada subfórmula Xφse cumple Xφ∈Ck−1si y solo si φ∈Ci. 2. Para cada subfórmula φ0Uφ1se cumple φ0Uφ1∈Ck−1si y solo si φ1∈Ck−1 oφ0∈Ck−1yφ0Uφ1∈Ci. Además, es necesario que si φ0Uφ0∈Cjpara algún jentre iyk, se tenga también φ1∈Cj′para un j′en el mismo rango. Esta condición se comprueba mientras se calculan los Cj. Por inducción estructural sobre la construcción de las fórmulas en LT L se tiene que ψ∈Cjsi y solo si w(j)w(j+ 1)...w(k−1)v∗|=ψ, donde ψes cualquier subfórmula de φ. Por ello, la palabra deseada es un modelo de φsi y solo si φ∈C0. Esto quiere decir que Macepta en este caso. Para terminar de probar la #PSPACE completitud, es necesario ver la #PSPACEdureza del problema. El modelo general de las demostraciones de dureza del análisis de complejidad de model counting para modelos de palabras periódicas se basa en la construcción de una fórmula φ∈ LT L que modeliza el comportamiento de una cierta máquina de Turing no determinista Mcon alguna restricción en tiempo y espacio en una entrada 24 Capítulo 3. Complejidad de distintos modelos de lógica temporal w. Dicha fórmula φcodifica las ejecuciones posibles en las que Macepta, por lo que la denotaremos φw M. La dificultad de este procedimiento reside en construir esta fórmula de tal manera que el número de ejecuciones en las que Macepta sea igual al número de modelos de φw Mpara cierto k, cota de la palabra periódica. Elegimos k de tal manera que una ejecución wde longitud maximal se pueda codificar en k−1 símbolos y definimos φw Mde tal manera que solo contenga modelos cuyo periodo tenga longitud uno, es decir, que el prefijo tenga k−1letras y el periodo solamente una. En caso de que una palabra que es modelo tenga longitud menor de k, basta con repetir la última letra hasta llegar a la longitud deseada y considerar esas letras añadidas como parte del prefijo. Teorema 3.2.3. Model counting con cadenas periódicas acotadas con kbinario es #PSPACE-duro. Demostración. Sea M= (Q, qt, QF,P, δ)una máquina de Turing no determinista de una cinta, donde Qes el espacio de estados, qtel estado inicial, Qfes el conjunto de estados en los que Macepta, Pes el alfabeto y δes la función de transición. Mrechaza cuando el estado final no es de aceptación. Sea Macotada en espacio por un polinomio p(n),w=w0...wn−1una entrada de My otro polinomio p′(n) (que solo depende de M) tal que Mtermina en un número 2p′(n)pasos, el máximo número de configuraciones distintas de la máquina si tenemos ese espacio, donde n es la longitud de la entrada. Esta máquina muestra el comportamiento de cualquier lenguaje en #PSPACE, de forma similar a la reducción de cualquier problema en NP a Circuit-SAT realizada en el teorema de Cook-Levin. El siguiente paso en la demostración es la construcción de la fórmula φw My una cota krepresentada en tamaño polinómico respecto a ntal que el número de ejecuciones en las que Macepta es el mismo que el número de palabras periódicas de longitud kque modelan φw M. Una ejecución de Msobre wse codifica por una secuencia finita de id’s idi, donde cada id es una descripción del estado de Men el instante i, incluyendo el contenido de la cinta, el estado de la máquina y la cabecera. Para ello se emplean lcproposiciones atómicas (representando los valores de bit de cada id). Por lo tanto, hay 2lc configuraciones distintas de la máquina. Esta sucesión se alterna con configuraciones ci, que están formadas por un símbolo único que indica si dos ids consecutivos son consistentes con la función de transición δde Mseguida por una repetición de un símbolo testigo: $id0#c0$id1#c1... $id2lc #c2lc (⊥)ω para un cierto lc(que se definirá más adelante). El periodo de la palabra es de la forma (⊥)lpara algún l > 0. Definimos ktal que las ejecuciones de longitud maximal de Men wpueden ser codificadas en el prefijo. Los símbolos cison únicos para cada i, lo cual hace que cada una de las 2lcconfiguraciones que son codificadas sean 3.2. Model Counting 25 diferentes (repitiendo la última configuración si es necesario hasta alcanzar el número deseado de configuraciones). Como la máquina se detiene por definición tras ese número de pasos, el periodo solo puede tener longitud 1. Esto asegura una relación 1:1 entre k-palabras y ejecuciones en las que Macepta. Sea lr=p(n)el tamaño maximal de la configuración de Men w. Para los ids se usa un contador binario con lc=p′(n)bits. Las proposiciones en Q∪Pse usan para codificar las configuraciones de Mcodificando el contenido de la cinta, el estado de la máquina y la posición de cabecera. Estas proposiciones representan los valores de bit de cada id. Los símbolos $y#se usan como separadores y el símbolo ⊥es un símbolo sin significado para representar el periodo del modelo. La distancia entre símbolos separadores es d=lr+3. Estamos en condiciones de definir φw Mcomo la conjunción de las siguientes fórmulas: 1. Id codifica los ids de las configuraciones. Emplea la fórmula Inc(b1, ...., blc, d) que afirma que el número codificado por los bits de bdespués de dpasos se obtiene incrementando el número codificado en la posición actual. 2. Init afirma que la ejecución de Mcomienza con la configuración inicial. 3. Accept afirma que la ejecución alcanza una configuración donde Macepta. 4. Loop define el periodo del modelo, solo puede contener ⊥. 5. Repeat afirma que la codificación de un estado aceptado se repite hasta que se alcance el id maximal. 6. Config declara la consistencia de dos configuraciones sucesivas con la relación de transición de M. Aquí, usamos doperadores Xpara relacionar la codificación de las dos configuraciones. La demostración de que todas las propiedades anteriores se pueden expresar con fórmulas de tamaño polinómico y la traducción de cada instrucción de Ma expresiones en LT L se puede ver en Torfah y Zimmermann (2014). Además, se necesita que cada fórmula especifique una serie de detalles: las proposiciones atómicas que codifican los ids no pueden aparecer en las configuraciones y viceversa; los separadores ($ y #) no pueden tener otros significados y aparecen únicamente 2p′(n)veces cada d posiciones; y las codificaciones de las configuraciones se representan con conjuntos únicos de letras de Pcon la excepción del conjunto de la cabecera, que contiene un símbolo de Q. Finalmente, se prueba que la fórmula tiene las propiedades deseadas: para k= 2lc∗(lr+ 3) + 1 (este número surge de las 2lcsecuencias de id y configuración precedidas por un $, donde la distancia entre un $ y el siguiente $ es lr+ 3 y el último símbolo añadido se debe al símbolo ⊥que representa el periodo), cada ejecución de Men una entrada wdonde Macepta corresponde con exactamente una palabra que modela φw Mque codifica esa ejecución en su prefijo. 26 Capítulo 3. Complejidad de distintos modelos de lógica temporal Por lo tanto, se cumple esa equivalencia entre ejecuciones y modelos. La fórmula φw Mse puede obtener en tiempo polinómico en |w|+|M|, y kes exponencial en |w|, con lo que puede ser codificado en binario con un número polinómico de bits. En base a los dos teoremas anteriores, se tiene el siguiente resultado: Corolario 3.2.3.1. El siguiente problema es #PSPACE-completo: Dado una fórmula LT L φy una cota kcodificada en binario, ¿cuántos modelos de palabras periódicas de longitud ktiene φ? Una vez hemos probado el resultado para la lógica LT L, surge la pregunta de considerar el problema para la otra lógica temporal que se ha planteado: LT L⋄. La versión de decisión de model counting en palabras periódicas para LT L⋄es NP-completa como resultado de un teorema de modelos pequeños, como se ve en Schnoebelen (2002). Este afirma que, en caso de existir algun modelo para la fórmula φ, existe uno de tamaño en O(|φ|). Si consideramos el problema de conteo asociado la situación es diferente. En efecto, debemos considerar cualquier modelo de tamaño k, no solo los de menor tamaño. Teorema 3.2.4. El siguiente problema es #P-completo: Dada una fórmula LT L⋄φ y una cota kcodificada de forma unaria, ¿cuántos modelos de palabras periódicas de longitud ktiene φ? Hemos observado que LT L⋄es un subconjunto de LT L y que la lógica proposicional usual está contenida en ella. Al haber resuelto este problema para ambas lógicas y haberse demostrado que es #P-completo, sabemos que se cumple este teorema, ya que al generalizar #SAT se trata de un problema #P-duro y al ser una particularización del problema análogo en LT L es #P-completo. Este resultado es poco relevante comparado con los que se tienen cuando k está codificado en binario, dado que usualmente se suele expresar la entrada en base computacional. Aquí el resultado es menos trivial, ya que model counting para LT L es #PSPACE-completo y no podemos saber con certidumbre la dificultad del problema por acotación. Sabemos que LT L⋄está en #PSPACE por ser una particularización de LT L, pero se ofrece una demostración de este hecho como muestra de cómo adaptar demostraciones de LT L aLT L⋄. Teorema 3.2.5. El siguiente problema está en #PSPACE: Dada una fórmula LT L⋄φ y una cota kcodificada en binario, ¿cuántos modelos de palabras periódicas de longitud ktiene φ? Demostración. Esta demostración va a proceder de forma muy similar al teorema 3.2.2. El esquema de la demostración consiste en adivinar una palabra uv letra a letra (denotamos la letra adivinada en un instante jcomo w(j)) y verificar en tiempo polinómico que esta palabra es un modelo para la fórmula φ. 3.2. Model Counting 27 La lógica LT L⋄puede expresarse con la lógica proposicional unida al operador □, cuyo significado recordamos. Se tiene que □φsi y solo si φse cumple siempre. Para verificar que uv |=φ, la máquina debe crear al comienzo un conjunto C0que contiene todas las subfórmulas de φque se satisfacen con la asignación inicial de valores en la primera letra de la palabra. Para una fórmula concreta, determinar el número de subfórmulas contenidas en ella es lineal y el espacio que requiere acumularlas es cuadrático. Con cada instante ise adivina la letra i-ésima de la interpretación uv y se actualiza el conjunto Ci, que es el que será almacenado, siguiendo el siguiente esquema: 1. La pertenencia a Cide proposiciones atómicas es determinado por w(i). 2. Las conjunciones, disyunciones y negaciones se comprueban localmente. Por ejemplo, ¬p∈Cjsi y solo si p /∈Cj. 3. Las fórmulas de la forma □ψaparecen en Cisi ψ∈Ciy□ψ∈Ci−1. Para cada instante ise almacenan únicamente dos conjuntos, Ci−1yCiy se tiene uv |=φsi φ∈Ck, donde kes el tamaño de la palabra, es decir, Ckes el último conjunto. Por tanto se tiene que la fórmula se verifica con un espacio asintóticamente constante y, por tanto, el problema está en #PSPACE. Parece entonces que el problema está entre #P y #PSPACE. Nos gustaría saber si es #P-completo o si, por otra parte, no está en #P, pero esta no es una distinción trivial. Para discutirlo volveremos a la definición de la clase #P, en la sección 2.3. Observamos que un problema de conteo pertenece a esta clase si existe una máquina de Turing no determinista Mtal que el número de caminos en los que Macepta es igual a la solución del problema de conteo. Si tenemos que una k-palabra es modelo de una cierta fórmula φpero Mno puede verificarla en tiempo polinómico, parecería lógico que no estuviera contenido en #P. Sin embargo, esto no es del todo correcto, ya que es posible que exista otra máquina M′distinta que cuente las ejecuciones de forma más eficiente. Un ejemplo de caso en el que ocurre un fenómeno similar es la determinación de la cantidad de números pares menor que un cierto número cdado. Este problema puede resolverse recorriendo todos los números menores que cy decidiendo si son pares (que en caso de estar ccodificado en binario conlleva un número exponencial de comprobaciones) o haciendo la división entera de centre 2, que es una operación constante en el tamaño de la entrada. Desconocemos si existe algún otro procedimiento, presumiblemente más eficiente, que pueda contar el número de certificados sin verificar ninguno. En caso de verificar alguno, el hecho de que este tuviera tamaño exponencial respecto al tamaño de la entrada implicaría que la comprobación no puede ser realizada en tiempo polinómico. Dado que no se conoce un método más eficiente de contar modelos para LT L ni para LP, parece razonable pensar que no existirá para 34 Capítulo 4. Conclusiones y Trabajo Futuro A lo largo del desarrollo de este estudio, se ha podido observar que algunas de las demostraciones presentadas, en particular la del teorema 3.2.3, son especialmente arduas tanto de comprender como de explicar de manera clara y accesible. Esto refleja la profundidad y la sofisticación inherente a estos temas, lo que subraya la necesidad de una mayor atención y estudio especializado en estos aspectos de la teoría de la complejidad y las lógicas temporales. En este trabajo se ha ofrecido por primer vez hasta donde sabemos un análisis de distintas versiones de model counting en LT L⋄para modelos de tamaño k. A modo de resumen se muestra una tabla con todos los resultados obtenidos, donde el resultados de no pertenencia de palabras periódicas con kbinario a #P está condicionado a la hipótesis de verificación necesaria, que indica que cada ejecución en una máquina de Turing que acepta debe codificar un modelo válido y los resultados de no pertenencia de k-árboles y k-grafos a alguna clase de equivalencia dependen de la hipótesis de almacenamiento necesario, una suposición más exigente que la anterior: kunario kbinario Palabras periódicas cota inferior #P-completo no en #P cota superior #PSPACE k-árboles cota inferior no en #PSPACE no en #EXPSPACE cota superior #EXPTIME #2EXPTIME k-grafos cota inferior #P-completo no en #PSPACE cota superior #EXPTIME En primer lugar, destacan las similitudes entre las complejidades de los modelos basados en palabras periódicas y k-grafos, similitud razonable si tenemos en cuenta que ambos tienen el mismo número de nodos. El caso de modelos basados en k-grafos es una generalización del caso de palabras periódicas, lo cual justifica el aumento de complejidad al considerar kcodificado en binario. Por otra parte, los modelos basados en k-árboles tienen un número exponencialmente mayor de nodos, por lo que resulta razonable que sean más complejos computacionalmente. Al observar la tabla, se observan pocos resultados de completitud, y los que se tienen son en #P, la clase de complejidad más estudiada de las que aparecen en este trabajo y cota inferior de la complejidad de cualquier model counting en lógicas temporales por ser estas generalización de la lógica proposicional usual. Esto se debe a la escasez de problemas #PSPACE-completos y #EXPSPACEcompletos conocidos a partir de los cuales hacer reducciones parsimónicas para demostrar la dureza de los problemas que se han estudiado. Una alternativa al uso de reducciones parsimónicas es el algoritmo usado en la demostración del teorema 35 3.2.3, que codifica las instrucciones y configuraciones de la máquina de Turing que se necesite en cada caso usando LT L⋄. Sin embargo, el autor no ha encontrado una manera de hacerlo, por lo que queda como trabajo futuro. Se especula que, al encontrar esta traducción para el caso en el que los modelos están formados por palabras periódicas de longitud k, donde k está codificado en binario, será sencillo probar la completitud para otras clases en el caso de modelos basados en k-árboles y k-grafos empleando traducciones similares. Además, los resultados relacionados con la no pertenencia a una determinada clase del conteo de modelos que satisfacen una fórmula en LT L⋄están condicionados por la inexistencia de un algoritmo de conteo más eficiente que el método explícito actualmente conocido, como se ha mencionado antes. Este método requiere que cada ejecución de una máquina de Turing considere de manera concreta cada interpretación posible y la valide. Determinar si la hipótesis de verificación necesaria es cierta, ya sea mediante una demostración rigurosa o a través de la contradicción de dicha hipótesis, es un paso esencial para completar este trabajo. Cap´ ıtulo 5 Introduction 5.1. Motivation The objective of mathematics, and science in general, is to define and explain the reality that surrounds us. Natural language is commonly used to explain what happens around us, but it is full of exaggerations, complexities and subtleties which make it difficult to perform a detailed study. For this reason, formal languages have been created. They facilitate the objective expression of situations and phenomena. Among formal languages, the ones that include time as a variable are specially useful when describing physical phenomena. For that purpose, several temporal logics have been defined, among which linear-time temporal logic or LT L, a logic that considers time as a linear flux, stands out. To formalise this kind of reasoning and determine whether a logical affirmation is true (or if it could be) is a relevant problem in mathematics and computation. The propositional satisfiability problem (SAT), which considers whether, for a certain formula, there is an interpretation of truth values to propositions which make it true, is responsible for the creation of thhe computational complexity analysis field. Originally, the analysis of the complexity of temporal logic formulas’satisfiablity was performed in Sistla y Clarke (1985). Other authors, such as Schnoebelen (2002), have researched variations of this problem, altering the temporal logics’semantics or analysing different models and variations of the satisfiability problem. Associated with the boolean satisfiability problem, we can define a counting problem, which analyses the total number of interpretations that satisfy a given formula, is defined. It is closely related to probability calculations and it is useful to determine if a formula tends to be true. Counting complexity in models of temporal logics was analysed in Torfah y Zimmermann (2014), where the computational complexity of the satisfiability problem for LT L was explored. This resulted in an idea to expand analogous results to other logics whose complexity has not been studied as of now. 37 38 Capítulo 5. Introduction 5.2. Research objectives The objective of this Bachelor’s thesis is to analyse the complexity associated with counting models that satisfy a LT L formula. These results are meant to be used to solve analogous problems with LT L⋄formulas. LT L⋄is a temporal logic strictly contained within LT L. Another objective is to increase understanding regarding temporal logics and complexity reasonings, mainly related with counting complexity. 5.3. Working plan This study was divided into two stages: 1. Research: First, counting complexity classes were studied, using chapter 17 of Arora y Barak (2006) as a starting point, as recommended by the tutors. Afterwards, spatio-temporal reasonings were researched to formalise the problem associated with determining the number of likely pasts for given present situations. The objective was to analyse the complexity of the feasible past determination problem for applied cases. Following a meeting with the tutors, it was decided to expand and generalise our focus to analyze temporal logics’complexity. With this new objective, a literature research regarding the complexity of counting problems in temporal logics. After finding, reading and understanding the article written by Torfah y Zimmermann (2014), it was agreed to investigate the complexity of counting the solutions to formulas in LT L⋄. 2. Development: Once the research objective was settled, the results obtained by other authors regarding the complexity of model counting in LT L formulas were used as a base for this study. New results about the complexity of the problem of counting the number of models of formulas LT L⋄were deduced and proven. Particularly, three different types of models in which satisfiability is deterministic were determined. An analysis of the complexity of counting the number of each model type that satisfied a formula in LT L⋄. 5.4. Work structure The rest of this study is divided in 5 chapters, following the structure presented below: 1. The chapter 2 acts as a preface. It introduces necessary concepts to understand the structure and results found in the next chapter. Relevant complexity classes (and a hierarchy among them) and the different logics that will be used as a base for the study are defined. 5.4. Work structure 39 2. The chapter 3 includes the bulk of this Bachelor’s thesis. It contains the author’s work, some new proven results and similar results found by other authors. 3. The chapter 4 consists of a brief summary of the results found in the previous chapter, their analysis and future work possibilities. 4. Finally, chapters 5 y 6 are English translations of chapters 1 and 4, respectively. Cap´ ıtulo 6 Conclusions and Future Work The analysis of computational complexity is fundamental for trying to understand inherent differences between various problems and algorithms. This analysis allows us to compare the efficiency of algorithms in terms of time and space required for their execution. It also helps us identify the most challenging problems and seek more efficient solutions for them. Additionally, as mentioned in the introduction, the formalisation of temporal reasoning is extremely useful to address issues related to physical phenomena. Knowing the computational complexity of determining whether a formalised physical reasoning can be true is essential in a great number of situations. This complexity can influence fields where precision and efficiency are crucial, such as physics, engineering, or computer science. Furthermore, it is highly useful to be able to determine the probability that a certain event will occur in the future or has occurred in the past, which can be trivially calculated by counting the number of situations in which this event takes place if each situation has the same probability. In any other case, a similar reasoning to counting paths will be required. The basic capacity of counting the number of situations in which something happens is therefore necessary. This ability is not only important in scientific and technological applications, but also in daily decision-making and risk assessment, where understanding probabilities can significantly enhance our judgements and decisions. Considering this, we can understand that the study of LT L and LT L⋄is extremely interesting and relevant across multiple fields of knowledge. These logics have important applications in areas such as system verification, artificial intelligence, and dynamic systems theory, among others. However, their understanding is complex and not comprehensively covered in the curriculum of this degree. Similarly, the classes of counting complexity, which are essential for understanding the inherent difficulty of counting problems, are not part of the usual course content neither, nor are many of the decision classes discussed in this project. 41 42 Capítulo 6. Conclusions and Future Work Throughout the development of this study, it has been observed that some of the presented demonstrations, particularly that of Theorem 3.2.3, are especially arduous to comprehend and to explain clearly and accessibly. This reflects the depth and sophistication associated to these topics. Furthermore, it also highlights the need for greater attention and specialised study in these aspects of complexity theory and temporal logics. In this work, we have offered, to the best of our knowledge, the first analysis of different versions of model counting in LT L⋄for models of size k. A summary table with all the obtained results is presented below: unary kbinary k Periodic words lower bound #P-complete not in #P upper bound #PSPACE k-trees lower bound not in #PSPACE not in #EXPSPACE upper bound #EXPTIME #2EXPTIME k-graphs lower bound #P-complete not in #PSPACE upper bound #EXPTIME Bear in mind that every result of non-inclusion to a certain class presented in the table above depends on the truthfulness of a certain hypothesis. First of all, periodic words with binary knot belonging to #P depends of the mandatory verification hypothesis. The results of non-inclusion for k-graphs and k-trees depend on a second more restrictive hypothesis, the mandatory storage hypothesis. First of all, the similarities between the complexities of models based on periodic words and k-graphs are noteworthy. This similarity is reasonable considering that both types of models have the same number of nodes. The case of models based on k-graphs is a generalisation of the case of periodic words. This justifies the increase in complexity when considering kencoded in binary. On the other hand, models based on k-trees have an exponentially larger number of nodes, which explains them being more computationally complex. Upon examining the table, few results of completeness are observed. Those that do exist are in #P, the most studied complexity class among the ones mentioned in this article. Moreover, since model counting of temporal logics is a generalisation of model checking for the usual propositional logic, #P is the lower bound of the complexity of any of these models. This scarcity is due to the limited number of known #PSPACE-complete and #EXPSPACE-complete problems, from which parsimonious reductions can be made to demonstrate the hardness of the studied problems. An alternative to parsimonious reductions is the algorithm used in the demonstration of Theorem 3.2.3, which en- 43 codes the instructions and configurations of the necessary Turing machine in each case using LT L⋄. However, the author has not found a way to achieve this, leaving it as future work. It is speculated that finding the translation for models consisting of periodic words of length k, where kis encoded in binary, will make it easier to prove completeness for other classes of models based on k-trees and k-graphs using similar translations. Moreover, the results related to the non-membership of a particular counting class for models that satisfy a formula in LT L⋄are conditioned by the lack of a more efficient counting algorithm than the currently known explicit method. The explicit method requires that each execution of a Turing machine considers each possible interpretation concretely and in detail. Determining the truthfulness of this assumption, either through rigorous demonstration or by contradicting the hypothesis, is an essential step to complete and strengthen the present work.