Ahora pasamos a la semántica. Al igual que para la lógica proposicional, definimos "modelo" y "satisfacción", aunque ahora necesitamos, también, el concepto de "trayectoria". Después, veremos un concepto adicional que es el de "equivalencia lógica". Un modelo tiene cuatro partes. Primero, necesitamos un conjunto "P" de variables proposicionales. Vamos a nombrar a estas variables con las primeras letras del alfabeto español. Además, nos dan un conjunto de estados. Los estados se van a llamar, por ejemplo, "s" y "t". Cada estado debe estar etiquetado con un conjunto de variables proposicionales. Suponemos una función "L" que va del conjunto "S" de estados al conjunto "potencia de p". Es decir, dado un estado, o sea, un elemento de "S", regresa un conjunto de variables, o sea, un elemento del conjunto "potencia de p". Finalmente, tenemos la relación "R" que es un conjunto de parejas de estados. Normalmente, se asume que "R" satisface la siguiente restricción: todo estado debe tener, al menos, una flecha que sale de él. O sea que para todo estado "s" hay una pareja de estados con "s" como primera componente. Una trayectoria es una sucesión infinita de estados que respeta a la relación. Siempre podemos construir una sucesión infinita porque todo estado tiene, al menos, una flecha que sale de él. Aquí vemos tres trayectorias que empiezan en "s". La primera abandona "s" en el segundo estado, y pasa a "t". La segunda trayectoria sale de "s" en el tercer estado. Y la tercera pasa a "t" en el cuarto estado. Es posible que haya más de una flecha que sale de un estado, cuando esto ocurre, se dice que el modelo es "no determinista". El no determinismo es útil para modelar, por ejemplo, decisiones tomadas por un agente externo al modelo. Supongamos que "a" denota que el homicida está fuera del compartimento de la víctima; "b", que el tren está en movimiento; y "c", que la víctima está muerta. El hecho de que "s" tenga una flecha hacia sí misma "s", y otra hacia "t", indica que no sabemos en qué momento el homicida va a decidir entrar al compartimento de la víctima. Ahora sí estamos listos para definir "satisfacción". Suponemos una trayectoria que denotamos con pi, que es una sucesión infinita de estados y que empieza en "s0", y fórmulas alfa y beta. Hasta la conjunción, la satisfacción coincide con la de lógica proposicional. Quizás, el único detalle que conviene resaltar es que una variable es cierta en una trayectoria si esa variable está entre las etiquetas del primer estado "s0" de esa trayectoria. Continuamos con los operadores temporales. Vamos, ahora, a usar superíndices para denotar sufijos de una trayectoria. Pi con superíndice "i" indica el resto de la trayectoria a partir del "i-ésimo" estado, empezando en "s0". "Pi super uno", entonces, es pi sin su primer estado, es decir, "pi super uno" es la trayectoria que resulta de avanzar un instante de tiempo hacia el futuro. Entonces, "X alfa" es cierto en pi si y sólo si alfa es cierto en la trayectoria que resulta de borrar el primer estado de pi. Pi hace cierta a "F alfa" si y sólo si existe un sufijo de pi que haga cierta a alfa, o sea, si alfa es cierta en algún instante presente o futuro. Pi hace cierta a "G alfa" si y sólo si los sufijos de pi hacen cierta a alfa, o sea, si alfa es cierta, siempre, en esa trayectoria. Vimos "satisfacción" para una trayectoria. Ahora necesitamos definir "satisfacción" para un modelo y un estado. En este caso, alfa se cumple en el estado "s" de un modelo si todas las trayectorias que salen de "s" hacen cierta a alfa. Por convención, arbitrariamente se eligen todas las trayectorias. Vamos a ver unos ejemplos; "a y b" es cierta en "s", porque tanto "a" como "b" son ciertas en el primer estado de todas las trayectorias que empiezan en "s". "Xb" es cierta en "s" porque "b" es cierta en el segundo estado de todas las trayectorias que parten de "s". "Fc", en cambio, no es cierta en todas las trayectorias que empiezan en "s". En particular, no es cierta la trayectoria que permanece en "s" hasta el infinito; nunca, en el futuro, aparece "b" en esa trayectoria. Por último, "Gb" es cierta para "M" y "s" porque se cumple en todos los estados de todas las trayectorias que salen de "s". Decimos que dos fórmulas son lógicamente equivalentes entre sí, si para todo modelo y toda trayectoria de ese modelo las trayectorias que hacen cierta a una fórmula, también hacen cierta a la otra fórmula. Así, podemos ver que "no F alfa" es lógicamente equivalente a "G no alfa", es decir, "F" y "G" son duales. También es posible demostrar que "F" distribuye sobre la disyunción y que se "G" distribuye sobre la conjunción. Terminamos con la inferencia en lógica temporal. Vamos a ver primero "satisfacción" y "validez", luego vamos a hablar de "verificadores de modelos", y vamos a terminar mencionando aplicaciones. En forma similar a como lo hicimos en la lógica proposicional, consideremos el problema de satisfacción y el de verificación de modelos. Satisfacción es: dada una fórmula "alfa", ¿existen un modelo y un estado de ese modelo que hagan cierta a alfa? En el problema de verificación de modelos, en cambio, nos dan no sólo alfa, sino también "M" y "s". Y nos preguntan si alfa es cierta en "M" y "s". El problema de verificación de modelos ha tenido un impacto enorme en la industria. Típicamente, "M" ya está dado y representa un sistema. Queremos saber si ese sistema tiene o no cierta propiedad representada por una fórmula "alfa". Un verificador de modelos es un programa de computadora que nos dice si, efectivamente, el sistema tiene, o no, esa propiedad. Los verificadores de modelos pueden, actualmente, verificar sistemas muy grandes con diez a la 20 estados o, a veces, mucho más grandes como diez a las 150 estados, o más. Esto es más que el número de átomos del universo conocido. Estos son ejemplos de sistemas que sólo se han podido analizar usando herramientas de lógica. Claramente, estos verificadores no representan cada estado explícitamente, sino que representan conjuntos de estados en fórmulas "booleanas". Dos métodos que funcionan así son los diagramas binarios de decisión y los resolvedores SAT, que vimos anteriormente. La principal aplicación de los verificadores de modelos es en la detección de errores en circuitos digitales. Más recientemente se han aplicado a encontrar errores en programación.