Título: Traducción automática de especificaciones Spectra a Modelos FSP
Directores: Hernán Gagliardi, Sebastián Uchitel
Jurados: Victor Braberman, Florencia Zanollo

Resumen
El problema de la síntesis de controladores consiste en construir automáticamente un sistema correcto por construcción que satisfaga un conjunto de objetivos, dadas ciertas suposiciones sobre su entorno. Para evaluar un nuevo algoritmo de síntesis composicional implementado en la herramienta desarrollada in-house MTSA, se necesitaban benchmarks.
La colección de especificaciones de Spectra (SYNTECH) era ideal, pero su modelo de juego era incompatible con el formalismo asincrónico y basado en eventos de MTSA.
Esta tesis presenta una traducción formal y automatizada. Se propuso un esquema de traducción que mapea de Spectra a un modelo MTSA que preserva la semántica original y se evaluó experimentalmente el rendimiento de la síntesis composicional sobre el benchmark traducido.
Los resultados fueron mixtos: si bien el enfoque composicional demuestra ser capaz de resolver ciertas clases de problemas que son intratables para el algoritmo monolítico, su efectividad depende críticamente de la heurística y la arquitectura del problema, siendo a veces superado por este.