On va considérer le script ci-dessous, qui calcule la somme des entiers consécutifs jusqu’à 5 :

Voici une simulation en mode pas-à-pas, où le temps $N$ est piloté par un curseur situé en bas de la figure (La ligne en cours d’exécution est coloriée en rouge, et on a abrégé « indice=indice+1 » en « indice++ ») :

JavaScript en mode pas-à-pas

Au temps $N=0$, les deux variables $indice$ et $somme$ sont indéfinies. Au temps $N=1$, la proposition $somme=0$ est vraie (effet de l’initialisation), et le reste tant que $N\leqslant 4$ : Après ça, quand $N=5$, $somme=1$ est vraie et donc $somme=0$ ne l’est plus !

Histoire d’avoir une notation, comme il est d’usage d’écrire $p$ juste pour dire que $p$ est vraie (et $\neg p$ si $p$ est fausse), notons $p_n$ le fait que $p$ est vraie au temps $n$ (c’est-à-dire lorsque $N=n$). Cela suppose que le temps est discret [1].

Par exemple, la proposition $somme=3$ est vraie aux temps $N=7$ et $N=8$ mais pas avant ni après :

$$\neg(somme=3)_2$$

mais

$$(somme=3)_7$$

et

$$(somme=1)_2$$

La logique temporelle est une logique modale, ce qui veut dire que non seulement une proposition $p$ peut être vraie ou fausse, mais qu’elle a plusieurs manières d’être vraie (par exemple, dans le futur ou dans le passé).

Le plus simple des opérateurs modaux de la logique temporelle est noté $\bigcirc$ et signifie « vrai au prochain top » (donc là encore, le temps est supposé discret et mesuré par des entiers naturels). Si l’intervalle de mesure du temps est le jour, $\bigcirc$ signifie « vrai le lendemain ».

Dans l’exemple de l’onglet précédent, on a

$\bigcirc (somme=3)_6$ puisque $(somme=3)_7$

$\neg \bigcirc(somme=3)_2$ puisque $\neg (somme=3)_3$

mais

$\bigcirc (somme=0)_3$ puisque $(somme=0)_2$

Plus généralement on a

$$\bigcirc p_n \Leftrightarrow p_{n+1}$$

Axiomes

L’opérateur $\bigcirc$ obéit aux axiomes suivants :

• $\neg\bigcirc p \Rightarrow \bigcirc \neg p$ (ce qui ne sera pas vrai demain, sera faux demain) ;
• $\bigcirc(p \wedge q)\Rightarrow \bigcirc p \wedge \bigcirc q$ (s’il pleut et vente demain, alors il pleuvra demain, et il y aura du vent demain) ;
• $\bigcirc(p \vee q)\Rightarrow \bigcirc p \vee \bigcirc q$ (s’il pleut ou vente demain, alors ou bien il pleuvra demain, ou bien il y aura du vent demain).

Toutes ces choses qui sont vraies seulement à certains moments mais pas tous, c’est bien compliqué. La logique temporelle s’intéresse beaucoup plus à ce qui est tout le temps vrai, avec ça au moins on est en terrain stable...

On note donc $\Box p$ le fait que $p$ est vrai mais aussi le restera toujours.

On a donc $\Box p \Rightarrow p$ mais aussi $\Box p \Rightarrow \bigcirc p$.

D’ailleurs $\Box p$ peut être défini récursivement par

(que $p$ soit destiné à être toujours vrai à partir de maintenant, signifie que $p$ est vrai et que son statut sera le même demain).

L’opérateur modal « toujours » ($\Box$) obéit aux axiomes suivants :

• $\Box(p \wedge q) \Leftrightarrow (\Box p \wedge \Box q)$
• $\Box p \Rightarrow \Box \Box p$ (l’éternité est éternelle)
• $\Box(p\Rightarrow q) \Rightarrow (\Box p \Rightarrow \Box q)$ (si une implication et sa prémisse sont toujours vrais alors sa conclusion l’est aussi)
• $\Box(p\Rightarrow \bigcirc p)\Rightarrow(p\Rightarrow \Box p)$ (si chaque fois que $p$ est vrai, il le reste le lendemain, alors dès que $p$ est vrai c’est pour toujours : C’est le principe de récurrence).

Il ne faut jamais dire jamais

Au lieu de noter le fait que $p$ n’est jamais vrai par $\Box \neg p$ on a aussi une notation duale : $\neg \Diamond p$ où $\Diamond p$ veut dire que $p$ sera vrai au moins une fois dans le futur (« $p$ est inéluctable »).

Alors $\Box p \Leftrightarrow \neg \Diamond \neg p$ et $\Diamond p \Leftrightarrow \neg \Box \neg p$ (l’inéluctable, c’est le pas toujours faux).

Une propriété dont on souhaite très fort qu’elle soit inéluctable en algorithmique, c’est l’arrêt d’un algorithme.

L’opérateur $\Diamond$ obéit à ces axiomes :

• $\Diamond(p \vee q)\Leftrightarrow (\Diamond p \vee \Diamond q)$
• $\Box p \Rightarrow \Diamond p$
• $\bigcirc p \Rightarrow \Diamond p$
• $\Diamond p \Rightarrow \Diamond \Diamond p$ (ce qui est inéluctable, est inéluctablement inéluctable : On dirait du Pierre Dac...)

En notant $P$ le prédicat « est président » et $N$ le prédicat « a pour nom », on a

$$\exists x, P(x)_{1968}\wedge N(x)=\mbox{de Gaulle}$$

$$\exists y, P(y) \wedge N(y)=\mbox{Sarkozy}_{1968}$$

La première interprétation est celle d’Alice, la seconde celle de Bob : La différence entre les deux est le prédicat sur lequel porte la propriété « en 1968 ».

Les deux ont raison !