Título: Definición y análisis de etapas de exploración on-the-fly para síntesis de controladores del tipo non-blocking
Directores: Sebastian Uchitel y Sebastian Zudaire
Jurados: Nicolas  D’ippolito y Florencia Zanollo

Resumen:

En el área de control supervisado se busca sintetizar de forma automática un «controlador» para un «Labeled Transition System» (o LTS), es decir una máquina de estados finita con sus transiciones etiquetadas (particionadas en controlables y no-controlables) y algunos estados marcados, que permite modelar formalmente un sistema de eventos discretos. Un «controlador» para un LTS es una función que dada una cadena de etiquetas restringe las etiquetas controlables posibles que pueden extenderla, con el objetivo de satisfacer una propiedad particular, que suele expresarse en fórmulas de lógicas como Linear Temporal Logic (LTL).

En trabajos previos se presentó un algoritmo para resolver este tipo de problemas para casos donde el LTS se da como la composición paralela de varios LTS’s más pequeños. El algoritmo de Directed Controller Synthesis (DCS) introduce una idea que permite explorar los automatas de forma incremental e ir componiendo solamente la parte explorada, haciendo uso de una heurística.

Nuestro objetivo es, por un lado, definir y entender en profundidad las etapas que atraviesa el algoritmo (DCS) durante su ejecución y cuantificar el rendimiento de las heurísticas actuales para cada fase.

Además buscamos introducir cambios a una heurística actualmente exitosa que impacte en una de las fases de ejecución cuyo rendimiento es menor en términos relativos.