Lógica de árbol de computación robusta

Resumen Se acepta ampliamente que cada sistema debe ser robusto en el sentido de que las violaciones "pequeñas" de las suposiciones del entorno deberían llevar a violaciones "pequeñas" de las garantías del sistema, pero no está tan claro cómo hacer que esta intuición sea matemáticamente precisa. Mientras que se han dedicado esfuerzos significativos a proporcionar nociones de robustez para la lógica temporal lineal, las lógicas de tiempo ramificado, como la lógica de árbol de computación (CTL) y CTL*, han recibido menos atención al respecto. Para abordar esta deficiencia, desarrollamos extensiones "robustas" de CTL y CTL*, a las que llamamos CTL robusta (rCTL) y CTL robusta* (rCTL*). Ambas extensiones son sintácticamente similares a sus lógicas madre, pero emplean semánticas multivaloradas para distinguir entre violaciones "grandes" y "pequeñas" de la especificación. Mostramos que la semántica multivalorada de rCTL la hace más expresiva que CTL, mientras que rCTL* es tan expresiva como CTL*. Además, demostramos que el problema de verificación de modelos, el problema de satisfacibilidad y el problema de síntesis para rCTL y rCTL* tienen la misma complejidad asintótica que sus contrapartes no robustas, lo que implica que se puede agregar robustez a las lógicas de tiempo ramificado de forma gratuita.