La lógica temporal, un tipo particular de lógica modal, se utiliza en informática en algunos lugares sorprendentemente diferentes: robótica, verificación formal e incluso semántica. En general, la lógica temporal resulta útil cuando se trata de sistemas reactivos .
La lógica temporal tiene dos modalidades: □ y ◇. □ φ significa “φ siempre se mantiene” y ◇ φ significa “φ eventualmente se mantendrá”. Tienen la relación habitual para la lógica modal: □ φ ⇔ ¬ ◇ ¬φ y ◇ φ ⇔ ¬ □ ¬φ. A veces, la lógica temporal se extiende con algunos operadores adicionales como ∘ para “siguiente” y ▹ para “entonces” (x▹y significa “x será verdadero, entonces y será verdadero”).
En la verificación formal, la lógica temporal puede usarse para establecer invariantes sobre el código, especialmente útil para sistemas distribuidos. Por ejemplo, puede representar fácilmente las propiedades de seguridad (“no sucederá nada malo”) y de vida (“algo bueno sucederá eventualmente”) mediante la lógica temporal. Una propiedad de seguridad se vería como □ ¬φ donde φ es “algo malo”; una propiedad vital sería ◇ φ donde φ es “algo bueno”. Su programa puede verificarse según las especificaciones temporales utilizando un verificador de modelos como Spin.
La robótica heredó el uso de la lógica temporal de la verificación formal de sistemas concurrentes. En robótica, podemos usar la lógica temporal para especificar los requisitos sobre el plan de un robot. Por ejemplo, podríamos especificar evitar obstáculos como: [math] \ lnot (o_1 \ lor o_2 \ lor \ ldots \ lor o_n) \ triangleright \ pi) [/ math]. Aquí el objetivo del robot es π; Esta declaración dice que tiene que evitar todos los obstáculos hasta que alcance π. Otro ejemplo son los objetivos de secuencia: [matemáticas] \ Diamond (\ pi_1 \ land \ Diamond (\ pi_2 \ land \ Diamond \ pi_3)) [/ math]; esto asegura que el robot primero visite π₁ luego π₂ luego π₃ en ese orden. Estas propiedades también se pueden verificar utilizando herramientas como Spin. Para obtener más detalles, eche un vistazo a esta descripción general del laboratorio UPenn’s Grasp: http://repository.upenn.edu/cgi/…
- ¿Alguien puede usar matemáticas abstractas para explicar el concepto chino de Wu (nada), que definitivamente no es 0? ¿Qué conclusiones interesantes se pueden hacer?
- ¿Cuál es la motivación detrás de la definición de verdadero como el valor de verdad de (A implica B) cuando A es falso independientemente del valor de verdad de B?
- ¿Cuál es el significado de modus ponens?
- ¿Cuál es el significado de la falacia del hombre enmascarado?
- ¿Cuál es un ejemplo simple y resuelto de lógica difusa?
Un uso ligeramente diferente de la lógica temporal es dar semántica a la programación reactiva funcional. La programación funcional reactiva presenta al programador dos tipos de datos “primitivos”: flujos de eventos y comportamientos. Una secuencia representa eventos discretos como las pulsaciones de teclas; puedes modelar un teclado como un Event Char que te daría un personaje cada vez que alguien presiona una tecla. Un comportamiento representa un valor que siempre existe pero que puede cambiar continuamente con el tiempo; Esto es bueno para cosas como la posición del cursor, que sería un Behavior (Int, Int) . Para una introducción más detallada, consulte: ¿Qué es la programación funcional reactiva?
Siguiendo a Curry-Howard, los eventos y comportamientos de FRP corresponden a la lógica temporal. En particular, los eventos son ◇ y los comportamientos son □. Esto es útil para razonar sobre programas reactivos funcionales, y también se utiliza para definir tipos dependientes para FRP. La idea básica es simple: primero, expresamos □ y ◇ usando el tiempo explícitamente:
[matemáticas]
\ begin {align}
\ square x & \ equiv \ forall t ‘\ in [t, \ infty). x_ {t ‘} \\
\ diamond x & \ equiv \ exist t ‘\ in [t, \ infty). x_ {t ‘}
\ end {alinear}
[/matemáticas]
Aquí [math] [t, \ infty) [/ math] es el dominio del tiempo, que puede ser cualquier conjunto totalmente ordenado y generalmente es continuo. El truco es que ◇ y □ ahora tienen un “tiempo de inicio” [matemático] t [/ matemático], que usaremos en nuestros tipos para asegurarnos de que solo combinemos flujos y comportamientos compatibles. Dada esta idea, podemos transcribirla fácilmente a tipos dependientes:
[matemáticas]
\ begin {align}
\ text {comportamiento} \ \ alpha & \ equiv \ Pi t ‘: \ mathbf {time}. \ alpha_ {t ‘} \\
\ text {stream} \ \ alpha & \ equiv \ Sigma t ‘: \ mathbf {time}. \ alpha_ {t ‘} \\
\ end {alinear}
[/matemáticas]
Esto nos permite hacer cumplir la “consistencia de la hora de inicio” utilizando nuestro sistema de tipos, lo que solo asegura que todos los valores reactivos sean válidos en el momento en que se usan, ya que los eventos y comportamientos pueden tener diferentes horas de inicio.
Entonces: la lógica temporal se usa para verificación formal, sistemas concurrentes, robótica e incluso tipos para programación funcional reactiva. Estoy seguro de que aún hay más cosas que me perdí.