| Autor(es) | Amir Pnueli (1941–2009); Edmund M. Clarke (1945–2020); E. Allen Emerson (n. 1954) |
| Fecha / periodo | 1977–1981 · Siglo XX · Israel y Estados Unidos |
| Tipo | Formal |
| Deriva de | Lógica temporal · Lógica de Hoare y lógica dinámica |
| Derivan de ella | — |
| Tres leyes | Identidad: ✓ (base clásica) · No contradicción: ✓ (base clásica en cada estado) · Tercio excluso: ✓ en cada estado y camino (\(\varphi \lor \neg\varphi\)), aunque \(\mathbf{A}\mathbf{F}p \lor \mathbf{A}\mathbf{F}\neg p\) no es válida |
La lógica de Hoare verifica programas que empiezan, calculan y terminan: su corrección se expresa con precondiciones y postcondiciones. Pero muchos sistemas no terminan nunca y no se juzgan por su resultado final: un sistema operativo, un protocolo de comunicación, el controlador de un ascensor. Lo que importa es su comportamiento a lo largo del tiempo: que nunca dos procesos entren a la vez en la sección crítica, que toda petición acabe siendo atendida. Pnueli vio que la lógica temporal de los filósofos era el lenguaje adecuado para expresar esas propiedades. Clarke y Emerson dieron el paso decisivo: en lugar de demostrar que un sistema cumple una fórmula, comprobar automáticamente que el modelo finito del sistema la satisface. El gesto distintivo es convertir una lógica modal en un algoritmo de verificación.
Estructuras de Kripke. Un sistema es \(M = (S, R, L)\): estados, una relación de transición total y un etiquetado de los estados con las proposiciones atómicas verdaderas en ellos. Un camino es una secuencia infinita \(s_0 s_1 s_2 \dots\) con \(s_i R s_{i+1}\).
LTL (Pnueli, «The temporal logic of programs», 1977). Operadores sobre un camino \(\sigma\):
Un sistema satisface \(\varphi\) si todos sus caminos desde el estado inicial la satisfacen.
Axiomatización de LTL (Gabbay, Pnueli, Shelah y Stavi, 1980), con las reglas de modus ponens y necesitación para \(\mathbf{G}\):
Propiedades típicas.
CTL (Clarke y Emerson, 1981). Cada operador temporal va precedido de un cuantificador de caminos: \(\mathbf{A}\) (en todos) o \(\mathbf{E}\) (en alguno). Así, \(\mathbf{AG}\varphi\), \(\mathbf{EF}\varphi\), \(\mathbf{A}[\varphi\,\mathbf{U}\,\psi]\). Las fórmulas se evalúan en estados, y el tiempo se ve como un árbol de futuros posibles.
CTL* (Emerson y Halpern, 1986) permite combinar libremente cuantificadores de caminos y operadores temporales, y contiene a ambas.
Expresividad. LTL y CTL son incomparables. \(\mathbf{F}\mathbf{G}p\) («a partir de algún momento, siempre \(p\)») es de LTL y no tiene equivalente en CTL. \(\mathbf{AG}\,\mathbf{EF}\,p\) («siempre es posible volver a \(p\)») es de CTL y no de LTL. Por el teorema de Kamp (1968), LTL con operadores de pasado tiene la misma expresividad que la lógica de primer orden sobre los naturales ordenados.
Complejidad y algoritmos.
Ejemplo. Un semáforo con estados rojo, verde y ámbar que cicla. La fórmula LTL \(\mathbf{G}(\mathit{rojo} \to \mathbf{X}\,\mathit{verde})\) se comprueba recorriendo las transiciones. La fórmula CTL \(\mathbf{AG}\,\mathbf{EF}\,\mathit{verde}\) asegura que desde cualquier estado alcanzable puede volver a ponerse verde. Si falla, el comprobador da un contraejemplo: un camino concreto que la viola.
Pnueli tomó su lógica de la tradición de la lógica temporal de Prior. No la leyó directamente en Prior, sino en Temporal Logic de Rescher y Urquhart (1971), de donde adaptó un sistema con tiempo discreto y lineal y operadores de futuro. Lo que cambió fue el modelo: los instantes pasan a ser estados de una ejecución, y el tiempo, una secuencia de pasos de cómputo. De la lógica de Hoare y de la verificación al estilo de Floyd hereda el objetivo, que es demostrar la corrección de programas; Pnueli extendió ese programa a los sistemas concurrentes y reactivos, donde las ternas de Hoare no bastan. CTL añade la ramificación, que en la lógica temporal filosófica había aparecido con el tiempo ramificado de Prior y Thomason.
La comprobación de modelos se desarrolló a la vez en Estados Unidos (Clarke y Emerson) y en Francia (Queille y Sifakis, 1982). Pnueli recibió el premio Turing en 1996; Clarke, Emerson y Sifakis, en 2007. Hoy la verificación con lógicas temporales es práctica industrial en el diseño de circuitos, protocolos, controladores y software crítico, y ha dado lenguajes normalizados como PSL. Para la pregunta «¿una lógica o muchas?» es un caso de especialización: la base proposicional es clásica, pero hay varias lógicas temporales incomparables, y la elección entre tiempo lineal y ramificado depende de qué propiedades se quieran expresar y de qué algoritmos se puedan usar. La utilidad computacional se convierte en criterio para elegir lógica.