La lógica temporal se puede ver como una extensión de la lógica proposicional. Como introducción, vamos a dar una definición informal de modelo para lógica temporal. Recordemos que en la lógica proposicional un modelo era una asignación de variables. Ahora, en cambio, un modelo va a consistir en varias asignaciones de variables. A cada asignación le vamos a llamar "estado". Dado un estado, solamente vamos a escribir las variables que tienen valor "cierto", como a veces hacÃamos para la lógica proposicional. Además, hay una relación entre estados. Un estado está relacionado con otro si es posible pasar de uno al otro en una unidad de tiempo. Aquà vemos un ejemplo de modelo temporal. Si tenemos tres variables "a", "b" y "c", en el estado "s", "a" y "b" valen "cierto", y "c" vale "falso". En el estado "t", "b" y "c" valen "cierto", y "a" vale "falso". Al transcurrir el tiempo, podemos salir del estado "s", para, ya sea, volver al estado "s" o pasar al estado "t". Una vez en el estado "t", sólo podemos regresar a él mismo. Después, vamos a dar una definición formal de modelo. Empezamos con la sintaxis. Hay muchas lógicas temporales. Aquà vamos a definir una lógica que se llama "lógica temporal lineal" o "LTL". Al igual que en la lógica proposicional, las fórmulas pueden ser "cima", "fondo", una variable proposicional, la negación de una fórmula, o la conjunción de dos fórmulas. No incluimos más operadores booleanos porque se pueden ver como abreviaturas de estos. Lo nuevo, ahora, son los operadores temporales. Estoy poniendo tres, pero puede haber más. Una fórmula precedida de "X" es también una fórmula. Intuitivamente, la "X" que viene de "next", en inglés, significa "mañana", o en el siguiente instante de tiempo. La "F" significa "futuro", y la "G", que viene de "global", significa "siempre".