Lògica temporal

De Viquipèdia
Dreceres ràpides: navegació, cerca
Per a altres significats vegeu «Lògica (desambiguació)».

La lògica temporal és un tipus de lògica modal usada per a descriure un sistema de regles i simbolismes per a la representació i el raonament sobre proposicions en les quals té presència el factor temps. Hi ha una certa relació amb altres varietats de lògica, per exemple, la lògica modal. El seu estudi té una certa importància dins l'estudi de la informàtica, en particular els desenvolupaments introduïts per Amir Pnueli.

Per exemple, prenguem la sentència: "Tinc gana"; encara que el seu significat és independent del temps, el valor de veritat o falsedat de la mateixa pot variar amb el temps en un determinat sistema que inclogui accions de menjar, així, en funció del sistema, algunes vegades serà certa i altres falsa, encara que mai serà certa i falsa simultàniament.

Història[modifica | modifica el codi]

La lògica temporal va ser estudiada per primera vegada per Aristòtil, en alguns dels seus escrits apareixen expressions que guarden una semblança amb una lògica temporal de primer ordre, així apareixen expressions amb quantificadors existencials i quantificadors universals, al costat de seqüències d'estats d'un ordre temporal, el que, en la pràctica és una lògica temporal.

Sistemes basats en lògica temporal[modifica | modifica el codi]

En lògica temporal apareixen els mateixos operadors que en una lògica de primer ordre, juntament amb altres de nous, entre els que es poden trobar: Sempre, algunes vegades i mai.

Alguns sistemes lògics basats en lògica temporal són: Lògica computacional en arbre (Computational tree logic, CTL), lògica linear temporal (Linear temporal logic, LTL) i Lògica temporal d'intervals (Interval temporal logic, ITL). Lògica d'accions temporal (Temporal Logic of Actions, TLA).

Operadors temporals[modifica | modifica el codi]

La lògica temporal té dues classes de operador és: operadors lògics i operadors modals (Stanford). Els operadors lògics són normalment operadors truth-functional (\neg,\or,\and,\rightarrow ). Els operadors modals fan servir el Linear Temporal Logic i Computation Tree Logic són definits com segueix.

Textual Símbólico Definición Explicación Diagrama'
Operadores binarios
\phi U \psi \phi ~\mathcal{U}~ \psi \begin{matrix}(B\mathcal{U}C)(\phi)= \\ (\exists i:C(\phi_i))\land(\forall j<i:B(\phi_j))\end{matrix} Until: \psi se cumple en el estado actual o uno posterior, y \phi se tiene que cumplir hasta esa posición. A partir de esa posición \phi no es necesario que se siga cumpliendo.
\phi R \psi \phi ~\mathcal{R}~ \psi \begin{matrix}(B\mathcal{R}C)(\phi)= \\ (\forall i:C(\phi_i))\lor(\exists j<i:B(\phi_j))\end{matrix} Release: \phi releases \psi si \psi se cumple hasta que la primera posición en la cual \phi se cumple (o siempre si dicha posición no existe).
Operadores unarios
X \phi \circ \phi \mathcal{N}B(\phi_i)=B(\phi_{i+1}) Next: \phi se cumple en el siguiente estado. (X es usado como sinónimo.)
F \phi \Diamond \phi \mathcal{F}B(\phi)=(true\mathcal{U}B)(\phi) Finally: \phi eventualmente se cumple (en algún lugar del camino).
G \phi \Box \phi \mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi) Globally: \phi se tiene que cumplir en todo el camino.
A \phi \begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix} All: \phi se tiene que cumplir en todos los caminos empezando en el estado actual.
E \phi \begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix} Exists: existe al menos un camino que parte en el estado actual en el cual \phi se cumple.


Símbols alternatius:

  • L'operador R de vegades denotat per V
  • L'operador W és l'operador weak until :  f W g és equivalent a  f U g \ o G f

Opearadores unaris són well-formed formula s cuandoquiera que B (\phi ) és ben format. Els operadors binaris són fórmules ben formades cuandoquiera que B (\phi ) i C (\phi ) són ben formades.

En algunes lògiques, alguns operadors no poden ser expressats. Per exemple, l'operador N no pot ser expressat en la Temporal Logic of Actions .

Equivalències[modifica | modifica el codi]

  1.  FRG =\neg (\neg f U\neg g)
  2.  Gf =\neg F (\neg f)
  3.  Ff = VUf on V = vertader
  4.  Af =\neg E (\neg f)
  5.  AXf =\neg EX (\neg f)

Exemple[modifica | modifica el codi]

Estructura Kripke d'exemple

A la figura es mostra una estructura de Kripke de tres estats. Es pot descriure de la següent manera:

  1. A l'estat vermell (i R ) es compleix p , i hi ha transicions cap a la resta dels estats.
  2. A l'estat verd (i V ) q és veritable, i les transciones van cap a l'estat blau o el mateix estat.
  3. A l'estat blau (i A ) són veritables q i r , i té una única transició, cap a l'estat verd.

Si es considera arbitràriament a l'estat vermell com estat inicial, es compleix el següent:

  • EX r: doncs prenent el camí i R i A i V i V ..., En el segon estat (i A ) r és vertader, amb el que es va trobar un camí que compleix X r.
  • AF q: doncs per qualsevol camí que s'esculli inevitablement caldrà entrar en els estats que fan complir q , és a dir, i V ae A .

Referències[modifica | modifica el codi]

  • Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic . Blackwell.
  • E. A. Emerson and C. Lei, modalities for model checking: branching time logic strikes back, in Science of Computer Programming 8, p 275-306, 1987.
  • E.A. Emerson, temporal and modal logic, Handbook of Theoretical Computer Science , Chapter 16, the MIT Press, 1990

Vegeu també[modifica | modifica el codi]

Enllaços externs[modifica | modifica el codi]