Un enfoque teórico de autómatas para la verificación de modelos en tiempo ramificado

La traducción de fórmulas de lógica temporal lineal a autómatas ha demostrado ser un enfoque efectivo para implementar la verificación de modelos en tiempo lineal y para obtener muchas extensiones y mejoras a este método de verificación. Por otro lado, para la lógica temporal ramificada, se ha pensado durante mucho tiempo que las técnicas teóricas de autómatas introducen una penalización exponencial, haciéndolas esencialmente inútiles para la verificación de modelos. Recientemente, Bernholtz y Grumberg 1993 han demostrado que esta penalización exponencial puede evitarse, aunque no lograron igualar la complejidad lineal de los algoritmos no teóricos de autómatas. En este documento, mostramos que los autómatas de árbol alternos son la clave para un marco teórico de autómatas completo para las lógicas temporales ramificadas. No solo pueden utilizarse para obtener procedimientos de decisión óptimos, como lo demostró Muller et al., sino que, como mostramos aquí, también hacen posible derivar algoritmos óptimos de verificación de modelos. Además, la simple estructura combinatoria que emerge del enfoque teórico de autómatas abre nuevas posibilidades para la implementación de la verificación en tiempo ramificado y nos ha permitido derivar mejores límites de complejidad espacial para este problema de larga data.