Tema de tesis

Creo que nunca he puesto nada técnico en este blog, pero después del difícil proceso de decisión para escoger un tema de tesis, me parece una buena idea intentar describir de qué va a tratar ésta. Espero que esto no resulte muy tedioso para el respetable :P.
Hace 10 meses, antes de llegar a Alemania, yo no sabía absolutamente nada de autómatas, y mis conocimientos de teoría de la complejidad eran absolutamente básicos. Ahora, he decidido hacer mi tesis sobre las condiciones que debe cumplir un autómata sobre árboles para que el problema de decidir si el lenguaje del autómata es vacío se pueda resolver utilizando espacio logarítmico.
Sé que la frase anterior resulta difícil de entender, por lo que quiero explicar un poco de qué se trata, y la motivación del mismo.
Es una práctica común actualmente utilizar autómatas para demostrar algunos resultados, sobre todo de decidibilidad (dificil palabra) en lógica. Por ejemplo, en lógica temporal lineal, se puede ver el estado con el paso del tiempo como una palabra infinita; así, si se quiere saber si alguna fórmula se satisface en esta lógica, se puede ver si cierto autómata (construído apropiadamente a partir de la fórmula) acepta alguna palabra. De igual forma, si se tiene lógica temporal que tiene ramificaciones al futuro, se utilizan autómatas que leen árboles.
El problema con este punto de vista es que la construcción del autómata es comúnmente exponencial, y muchas veces el problema de satisfacción no requiere tanta complejidad. Por ejemplo, en lógica temporal lineal, el problema de satisfacción es bien sabido que es PSpace-completo (o sea, requiere un espacio polinomial para ser resuelto). Entonces, cómo usar autómatas para obtener resultados similares?
Lo que se hace es que no se construye realmente el autómata completo, sino que se demuestra que se puede ir construyendo "según se necesite", y que la información necesaria en todo momento para hacer esta construcción, y mantener el estado adecuadamente, es polinomial. Además, debe existir una cota en la profundidad del árbol (un resultado intermedio que requiera que, si el autómata acepta un árbol, entonces debe aceptar un árbol de a lo más cierta profundidad) que se requiere también sea polinomial.
Lo que se logra con esto es probar que se puede utilizar espacio logarítmico en el tamaño del autómata (que viene a ser polinomial en el tamaño del problema original) para resolver el problema.
Estas demostraciones son comúnes, pero cada vez que se requiere, se hace una nueva "a la medida" para la lógica y el autómata en cuestión.
La idea para mi tesis es encontrar condiciones suficientes para que un autómata acepte una solución en espacio logarítmico del problema. De esta forma, cada vez que se quiera demostrar que el problema de satisfacción de cierta lógica está en PSpace utilizando técnicas de autómatas, simplemente se tiene que demostrar que el autómata en cuestión cumple estas condiciones.
Si da tiempo, y todavía tenemos ganas de seguir en esto, vamos a hacer lo mismo para otras clases de complejidad, como ExpTime. Ahí uno se topa con más problemas porque, mientras PSpace = NPSpace, ExpTime =/= NExpTime, y algunas de las técnicas (en particular, el clásico "adivino los estados que toma el autómata para aceptar este árbol" ya no son válidos, pues mandan directamente a la clase no-determinista.

Espero haber sido claro en mi explicación, si cualquiera está interesado, o tiene dudas, por favor no duden en contactarme.
Si no los aburrí demasiado, estoy pensando en tal vez poner una serie de posts explicando las bases de la teoría de autómatas, que es bastante básica.