¿Cuál es la diferencia entre LTL y CTL?

Ya leí ejemplos de fórmulas en CTL pero no en LTL y viceversa, pero tengo problemas para comprender mentalmente las fórmulas de LTL y realmente cuál es, en el fondo, la diferencia.

Para comprender realmente la diferencia entre LTL y CTL, debe estudiar la semántica de ambos idiomas. Las fórmulas LTL denotan propiedades que se interpretarán en cada ejecución de un programa. Para cada posible ejecución (una ejecución), que se puede ver como una secuencia de eventos o estados en una línea, y es por eso que se denomina "tiempo lineal", se verifica la satisfacción en la ejecución sin posibilidad de cambiar a otra ejecución durante la comprobación Por otro lado, la semántica CTL verifica una fórmula en todas las ejecuciones posibles e intentará todas las ejecuciones posibles ( operador A ) o solo una ejecución ( operador E ) cuando se enfrenta a una rama.

En la práctica, esto significa que algunas fórmulas de cada idioma no se pueden establecer en el otro idioma. Por ejemplo, la propiedad de reinicio (una propiedad de accesibilidad importante para el diseño de circuitos) establece que siempre existe la posibilidad de que se pueda alcanzar un estado durante una ejecución, incluso si nunca se alcanza realmente ( reinicio de AG EF ). LTL solo puede indicar que el estado de restablecimiento se ha alcanzado realmente y no que se puede alcanzar.

Por otro lado, la fórmula LTL no se puede traducir a CTL. Esta fórmula denota la propiedad de estabilidad: en cada ejecución del programa, s finalmente será verdadero hasta el final del programa (o para siempre si el programa nunca se detiene). CTL solo puede proporcionar una fórmula que sea demasiado estricta ( AF AG s ) o demasiado permisiva ( AF EG s ). El segundo está claramente equivocado. No es tan sencillo para el primero. Pero AF AG s es erróneo. Considere un sistema que realiza un bucle en A1 , puede ir de A1 a B y luego irá a A2 en el próximo movimiento. Entonces el sistema permanecerá en◊ ◻ $\Diamond\Box s$A2 estado para siempre. Entonces "el sistema finalmente permanecerá en un estado A " es una propiedad del tipo . Es obvio que esta propiedad se mantiene en el sistema. Sin embargo, AF AG no puede capturar esta propiedad ya que lo contrario es cierto: hay una ejecución en la que el sistema siempre estará en el estado desde el que finalmente se ejecuta una ejecución en un estado no A.$\Diamond\Box s$

No sé si esto responde a su pregunta, pero me gustaría agregar algunos comentarios.

Se discute mucho sobre la mejor lógica para expresar propiedades para la verificación de software ... pero el verdadero debate está en otro lugar. LTL puede expresar propiedades importantes para el modelado del sistema de software (imparcialidad) cuando el CTL debe tener una nueva semántica (una nueva relación de satisfacción) para expresarlas. Pero los algoritmos CTL suelen ser más eficientes y pueden usar algoritmos basados ​​en BDD. Entonces ... no hay mejor solución. Solo dos enfoques diferentes, hasta ahora.

Uno de los comentaristas sugiere el artículo de Vardi "Ramificación versus tiempo lineal: enfrentamiento final" .

Si se le da un objeto (por ejemplo, traza en caso de LTL), considera solo un futuro para cada punto en el tiempo, en CTL tiene una gran cantidad de ellos.

En particular, nextofrece una acción única en LTL pero (potencialmente) un conjunto completo en CTL.