11. Logica temporal
La lógica temporal se presenta como una extensión de la lógica proposicional, y se introduce a través de la definición de un modelo temporal.
Modelo Temporal
- Un modelo consiste en varias asignaciones de variables, denominadas "estados".
- La relación entre estados se establece si es posible pasar de uno a otro en una unidad de tiempo.
Definición Formal de Modelo
- Se define la "lógica temporal lineal" (LTL), que incluye fórmulas similares a las de la lógica proposicional.
- Se introducen operadores temporales: "X" (next), "F" (futuro) y "G" (global), que representan diferentes aspectos del tiempo en las fórmulas.
La lógica temporal es una rama de la lógica formal que se utiliza para razonar sobre proposiciones cuyo valor de verdad depende del tiempo. A diferencia de la lógica clásica, que analiza enunciados estáticos (verdaderos o falsos sin considerar cuándo), la lógica temporal introduce el tiempo como una dimensión esencial, permitiendo expresar y verificar cómo cambian los hechos a lo largo del tiempo.
Concepto general de lógica temporal
En la lógica temporal, no solo interesa si una proposición es verdadera o falsa, sino en qué momento lo es y cómo evoluciona en el tiempo. Esto resulta fundamental para modelar sistemas dinámicos, como programas informáticos, sistemas reactivos, procesos concurrentes y protocolos de comunicación, donde el comportamiento depende de secuencias de eventos.
Por ejemplo, se puede expresar que “un sistema eventualmente responderá a una solicitud” o que “si ocurre un evento, entonces siempre después ocurrirá otro”, afirmaciones que no pueden representarse adecuadamente con la lógica proposicional tradicional.
Elementos básicos
La lógica temporal parte de proposiciones atómicas y operadores lógicos clásicos (¬, ∧, ∨, →), pero añade operadores temporales que hacen referencia al tiempo. El tiempo puede concebirse como discreto o continuo, y como una línea lineal o una estructura ramificada, según el tipo de lógica temporal que se utilice.
Principales operadores temporales
Algunos de los operadores más comunes son:
-
X (neXt / siguiente): una proposición será verdadera en el siguiente instante.
-
F (Finally / eventualmente): una proposición será verdadera en algún momento del futuro.
-
G (Globally / siempre): una proposición será verdadera en todos los instantes futuros.
-
U (Until / hasta): una proposición es verdadera hasta que otra lo sea.
Estos operadores permiten expresar propiedades como seguridad (algo malo nunca ocurre) y vivacidad (algo bueno ocurrirá en algún momento).
Tipos de lógica temporal
Existen varias formas de lógica temporal, entre las más importantes destacan:
-
Lógica Temporal Lineal (LTL): el tiempo se modela como una secuencia lineal de estados. Se usa para describir propiedades que deben cumplirse a lo largo de todas las ejecuciones posibles de un sistema.
-
Lógica Temporal de Árbol de Computación (CTL): considera múltiples futuros posibles, representados como un árbol de ejecuciones. Permite razonar sobre la existencia o necesidad de ciertos comportamientos.
-
CTL*: combina las expresiones de LTL y CTL, siendo más expresiva, aunque también más compleja.
Trayectoria
En el contexto de la lógica temporal, una trayectoria es la secuencia ordenada de estados que sigue un sistema a lo largo del tiempo. Representa cómo evoluciona el sistema desde un estado inicial hacia estados posteriores, mostrando qué proposiciones son verdaderas en cada momento.
un superíndice es una forma de denotar partes específicas de una trayectoria. Imagina que tienes una secuencia de estados, como si fueran los pasos de una historia que se desarrolla en el tiempo. Cada estado en esta secuencia puede ser representado por un número, y el superíndice nos ayuda a identificar desde qué punto de la secuencia estamos hablando.
relatedInteligencia Artificial