Lògica temporal

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 seu valor de veritat o falsedat pot variar amb el temps en un determinat sistema que inclogui accions de menjar; així, en funció del sistema, algunes vegades serà certa i d'altres falsa, encara que mai serà certa i falsa simultàniament.

Història

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 que, en la pràctica és una lògica temporal.

Sistemes basats en lògica temporal

En lògica temporal, apareixen els mateixos operadors que en una lògica de primer ordre, juntament amb d'altres de nous, entre els quals 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 temporal lineal (Linear temporal logic, LTL), lògica temporal d'intervals (interval temporal logic, ITL) i lògica d'accions temporal (temporal logic of actions, TLA).

Operadors temporals

La lògica temporal té dues classes d'operadors: operadors lògics i operadors modals (Stanford). Els operadors lògics són normalment operadors de funcions de veritat (truth-functional: $\neg ,\lor ,\land ,\rightarrow$ ). Els operadors modals fan servir la lògica linear temporal (linear temporal logic) i la lògica computacional en arbre (computation tree logic) i són definits com segueix:

Textual	Símbòlic	Definició	Explicació	Diagrama
Operadors binaris
$\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}}$	Fins: $\psi$ s'acompleix en l'estat actual o un de posterior, i $\phi$ s'ha d'acomplir fins a aquesta posició, a partir de la qual, $\phi$ no cal que continuï acomplint-se.
$\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}}$	Alliberament: $\phi$ alliberaments $\psi$ si $\psi$ s'acompleix fins que la primera posició en què $\phi$ s'acompleix (o sempre si aquesta posició no existeix).
Operadors unaris
X $\phi$	$\circ \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	Següent: $\phi$ s'acompleix en l'estat següent (X s'usa com a sinònim).
F $\phi$	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true{\mathcal {U}}B)(\phi )$	Finalment: $\phi$ eventualment s'acompleix (en algun lloc del camí).
G $\phi$	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Global: $\phi$ s'ha d'acomplir en tot el camí.
A $\phi$		${\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}$	Tots: $\phi$ s'ha d'acomplir en tots els camins començant en l'estat actual.
E $\phi$		${\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}$	Existeix: existeix com a mínim un camí que surt en l'estat actual en què $\phi$ s'acompleix.

Símbols alternatius:

L'operador R,de vegades denotat per V
L'operador W és l'operador feble fins (weak until): $fWg$ és equivalent a $fUg\ oGf$

Operadors unaris són fórmules ben formades (well-formed formula) sempre que B ( $\phi$ ) és ben format. Els operadors binaris són fórmules ben formades sempre 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 lògica d'accions temporal (temporal logic of actions).

Equivalències

$FRG=\neg (\neg fU\neg g)$
$Gf=\neg F(\neg f)$
$Ff=VUf$ en què V = vertader
$Af=\neg E(\neg f)$
$AXf=\neg EX(\neg f)$

Exemple

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

A l'estat vermell (i_R) es compleix p, i hi ha transicions cap a la resta dels estats.
A l'estat verd (i_V) qés veritable, i les transicions van cap a l'estat blau o el mateix estat.
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 l'estat vermell com a estat inicial, es compleix el següent:

EX r: puix prenent el camí i_R i_A i _V i _V ..., en el segon estat (i_A) r és vertader, amb el qual es troba un camí que compleix X r.
AF q: puix 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

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.