Análisis de complejidad de lógicas temporales

Abstract

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 o LT 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⋄.

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 k-graphs. 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.