Logique(s) temporelle(s)

par Philippe Muller

Instants, intervalles et éventualités

Les représentations du temps peuvent se distinguer par les objets primitifs qu'elles considèrent, soit des "instants", points dans le temps sans durée, soit des objets étendus, "intervalles de temps". Il faut distinguer aussi ontologiquement plusieurs sortes d'entités "temporelles" centrales à toute théorie du temps et du changement. Nous avons d'une part des "temps" absolus (instants ponctuels ou intervalles de temps ayant une durée) qui permettent de dater et d'autre part des "états" (situation du monde stable par rapport à une propriété) et des événements (qui provoquent un changement de la situation du monde). On peut distinguer alors trois grandes méthodes pour la modélisation du temps et du changement d'un point de vue logique : il existe d'une part une tradition de tense logics qui considère des opérateurs temporels, introduit généralement comme des opérateurs modaux F et P (cf. Logique(s) modale(s)) : par exemple l'opérateur F est un opérateur de possibilité interprété comme suit : Fp signifie "il existe un moment dans le futur où p est vrai" et P est l'opérateur pour le passé; les propriétés de la relation d'accessibilité des mondes dans les modèles de Kripke déterminent alors la structure temporelle résultante sur l'ordre sous-jacent. L'alternative est de réifier les instants ou les intervalles de temps sur lesquels des propositions logiques sont valides ; c'est le cas du calcul des situations par exemple de la théorie de l'action de [Allen, 1984] et de ses successeurs. Par exemple, le langage utilisé est formé d'expression du type champion(france,coupe_du_monde),<math>I_98</math>) pour indiquer que la proposition champion(france,coupe_du_monde) est valide sur l'intervalle <math>I_98</math>. Un autre genre d'approche plus simple logiquement est caractérisée par une réification des entités temporelles en les introduisant comme arguments des prédicats dans une théorie du premier ordre. On peut alors traduire

(1) Le but en or a été marqué à la 114e minute par Laurent Blanc.

par <math>marque(LB,but,t)</math> où t correspond à l'instant où le but a été marqué. On peut aussi réifier les événements que l'on veut caractériser, à la façon de Davidson. Dans un article classique [Davidson, 1967] propose en effet de représenter la phrase :

(2) John buttered a toast at midnight with a knife.

Par la formule <math>buttered(john,toast,e)\land at(midnight,e)\land with(knife,e)</math> ce qui permet d'inférer séparément les caractéristiques de l'événement, par exemple que

(3) John buttered a toast at midnight.

Cette dernière approche à l'avantage d'introduire explicitement des individus ayant une extension temporelle et de rester dans un cadre de logique du premier ordre. Pour plus de précisions, les articles qui offrent un panorama sur les théories du temps sont légion, cf par exemple [Landman, 1991, van Benthem, 1995, van Benthem, 1983].

Logiques temporelles d'instants

Pour pouvoir comparer les structures temporelles pour entités étendues dans le temps (événements ou intervalles) il faut considérer les propriétés courantes des ordres caractérisant diverses théories temporelles à base d'instants. On parlera d'ordre sous-jacent à une représentation d'intervalles en parlant de la structure d'instants isomorphe sous-jacente si l'on considère un intervalle de temps comme un ensemble de points. On verra en fait précisément plus bas quels sont les liens que l'on peut faire entre les diverses représentations. Les structures d'instants sont des structures du type <math>I =\langle T,<\rangle</math> où <math>T</math> est un ensemble d'instants et où <math><</math> est un ordre partiel strict (irréflexif, transitif) qui peut avoir les propriétés supplémentaires suivantes :

Linéarité

<math>\forall x \forall y \quad (x<y \lor y<x \lor y=x)</math>

Succession

(correspond à l'infinité vers le passé et le futur)

<math> (\forall x \exists y \;\; y<x) \land (\forall x \exists y \;\; x<y)</math>

Densité

<math> \forall x \forall y (x<y\rightarrow \exists z \; x<z<y)</math>

Ordre Discret

<math> \forall x \forall y \; ((x<y\rightarrow \exists z (x<z \land \neg\exists u (x<u<z)))\land (x<y\rightarrow \exists z (z<y \land \neg\exists u (z<u<y))))</math>

Les deux derniers axiomes sont évidemment incompatibles. Un bon nombre de théories supposent la linéarité de l'ordre sous-jacent, sauf les approches qui considèrent le futur comme indéterminé et modélisable par une structure munie de branches représentant les alternatives possibles à partir d'un point (le calcul des situations est un exemple typique), ou bien celles qui considèrent le passé comme mal connu avec diverses histoires envisageables. Il faut noter que la théorie des ordres munis de la linéarité, la succession et la densité d'une part, et les théories des ordres munis de la linéarité, la succession et la discrétion d'autre part sont syntaxiquement complètes (tout ce que l'on peut énoncer dans ces théories est soit un théorème, soit la négation d'un théorème). Un modèle canonique de la première est l'ensemble des rationnels, un modèle canonique de la seconde est l'ensemble des entiers relatifs\footnotcf. [van Benthem, 1983]. Dans la limite des ordres linéaires il faut noter que les réels sont aussi un modèle des ordres denses, mais qu'ils ne sont pas complètement caractérisés par un tel ordre, ni par aucune théorie du premier ordre. Pour plus de détail sur les ordres, cf. la fiche correspondante Structures d'ordre.

Logiques d'intervalles

Quand on passe aux représentations temporelles à base d'intervalles le choix devient bien plus vaste que pour les instants.

Structures basées sur inclusion ou recouvrement

D'après [van Benthem, 1983] une structure d'intervalle est de la forme <math>T =\langle I,\sqsubseteq,< \rangle</math>. Les relations d'inclusion (<math>\sqsubseteq</math>) et de précédence <math><</math> peuvent avoir les propriétés suivantes (les noms des axiomes sont repris et traduits de van Benthem).

Transitivité

<math>x\sqsubseteq y \sqsubseteq z \rightarrow x\sqsubseteq z</math>

Réflexivité

<math> x\sqsubseteq x</math>

Antisymétrie

<math>x\sqsubseteq y \sqsubseteq x \rightarrow x=y</math>

Liberté1

<math> (\forall z \; (z\sqsubseteq x \rightarrow z\sigma y))\rightarrow x\sqsubseteq y</math> avec une définition du recouvrement temporel comme suit : <math>x\sigma y\equiv \exists u \; (u\sqsubseteq x \land u\sqsubseteq y)</math>

Orientation

<math>\forall x\forall y\exists u \; (x\sqsubseteq u \land y\sqsubseteq u)</math>

La relation de précédence <math><</math> peut avoir des propriétés analogues à la précédence portant sur des instants : transitivité, irréflexivité, et succession. La linéarité ne peut s'exprimer de façon similaire, mais on peut la modifier pour obtenir quelque chose d'analogue. De même la notion de densité doit être revue :

Linéarité<math>\;^*</math>

<math>x<y \lor y<x \lor x\sigma y</math>

Densité<math>\;^*</math>

<math>\forall x \exists y_1 \exists y_2 \; (x=y_1+y_2)</math>

avec la définition méréologique (cf méréologie)de la somme :

<math>x+y=(\iota z \; (x\sqsubseteq z \land y\sqsubseteq z)\rightarrow (\exists u \forall v (v\sigma u)\leftrightarrow (v\sigma x \vee v\sigma y)))</math>

Les liens entre <math><</math> et <math>\sqsubseteq</math> peuvent maintenant être précisés :

Incompatibilité

<math>x<y\rightarrow \neg x\sigma y</math>

Monotonie

<math>(x<y\rightarrow \forall u \; (u\sqsubseteq x \rightarrow u<y))</math>

(monotonie gauche)

<math>(x<y\rightarrow \forall u \; (u\sqsubseteq y \rightarrow x<u))</math>

(monotonie droite)

Ordre sur l'union d'intervalles

<math>(x<y \rightarrow \forall z \; ( z<y \rightarrow x+z<y)) \land (y<x \rightarrow \forall z \; ( y<z \rightarrow y<x+z))</math>

Convexité

<math> x<y<z \rightarrow \forall u \; ((x\sqsubseteq u \land z\sqsubseteq u \rightarrow y\sqsubseteq u))</math>

Liberté2

<math> (\neg x<y)\rightarrow \exists u \exists v \; (u\sqsubseteq x \land v\sqsubseteq y \land (\forall z\forall w ((z\sqsubseteq u \land w\sqsubseteq v)\rightarrow \neg z<w)))</math>

Le dernier axiome exprime que deux intervalles qui ne se précédent pas l'un l'autre peuvent avoir des sous-intervalles qui se précédent mais qu'ils doivent avoir des sous-intervalles qui n'ont plus cette propriété. Les axiomes de "liberté" sont appelés axiomes "témoins" (witness) par Landman [Landman, 1991], car ils affirment l'existence d'intervalles qui permettent de faire le lien entre une structure d'intervalles et une structure de points correspondant à un ordre sous-jacent (cf dernière section). Il faut noter que des axiomatisations presque équivalentes (à l'exception de la convexité des périodes temporelles) peuvent être obtenues à partir de la relation de recouvrement <math>\sigma</math> et de celle de précédence, en posant (cf [Kamp, 1979])

Symétrie de <math>\sigma</math> :	<math>x\sigma y\rightarrow y\sigma x</math>
Réflexivité de <math> \sigma</math> :	<math> x \sigma x </math>
Incompatibilité :	<math>x<y\rightarrow \neg x\sigma y</math>
Transfert :	<math> (x<y\land y\sigma z \land z<t)\rightarrow x<t</math>
Linéarité :	<math> x<y \lor x\sigma y \lor y<x</math>
L'inclusion :	<math>x\sqsubseteq y\equiv \forall z \; ((z\sigma x \rightarrow z\sigma y) \land (z<y\rightarrow z<x) \land (y<z\rightarrow x<z))</math>

Cette axiomatisation retrouve alors pour l'inclusion les propriétés d'ordre partiel et de monotonie.

Structures basées sur une relation de "contact" ("meet")

Les structures du temps d'Allen [Allen, 1984] sont des théories très populaires en informatique et ont été développées indépendamment de la tradition logique des logiques d'intervalles (comme l'a noté Galton, elles sont à rapprocher de la logique de [Hamblin, 1971]). Ce calcul d'intervalles a pour origine la nécessité de raisonner sur des processus ayant une certaine durée, ce qui n'était pas permis par les théories de l'action de l'époque en intelligence artificielle. Dans cette optique Allen ne considère d'abord que des intervalles et ignore les instants, les considérant comme étrangers au sens commun. Toutes les relations intuitives souhaitables pour pouvoir parler d'ordre temporel sont dérivées d'une unique primitive "meets" qui exprime que deux intervalles se touchent sans se recouvrir. Cette relation est axiomatisée comme suit (nous citons les axiomes de [Allen & Ferguson, 1994], en notant

<math>x||y \equiv meets(x,y)</math>

<math>x||y||z \equiv meets(x,y)\land meets(y,z)</math>)

• <math>(x||y \land x||z \land t||y)\rightarrow t||z </math>

Les intervalles définissent une classe d'équivalence des intervalles qui les rencontrent.

• <math>[\forall x\forall z (x||y||z \land x||u||z)] \rightarrow u=y</math>

Deux intervalles qui rencontrent les mêmes intervalles sont égaux.

• <math>\forall x \exists y\exists z \; (x||y\land z||x)</math>

Le temps est infini et les intervalles sont finis.

• <math>x||y||z||t \rightarrow \exists u \; (x||u||t)</math>

Ceci introduit des intervalles "sommes" de deux intervalles <math>y</math> et <math>z</math> qui se rencontrent.

• <math> (x||y \land u||v)\rightarrow (x||v \oplus \exists z \;

(x||z||v) \oplus \exists z \;(u||z||y))</math> Cet axiome exprime la linéarité de l'ordre sous-jacent : pour deux paires d'intervalles qui se rencontrent, soit le "point" de rencontre est le même, soit il existe un intervalle entre ces deux points de rencontre (et l'un de ces points est avant l'autre).

On peut alors définir 13 relations qui expriment tous les cas possible d'ordre entre les extrémités d'un intervalle de temps connexe. La caractéristique principale de cette théorie par rapport aux logiques temporelles présentées précédemment est (en dehors de son économie de primitives) l'indétermination par rapport à la densité (ce qui la rend incomplète).

Correspondances entre instants et intervalles

Nous avons vu rapidement les grandes options que l'on peut prendre quand on cherche à représenter logiquement le temps (instants ou intervalles) ; nous allons voir quels sont les liens formels que l'on peut faire entre les structures à base de points ou d'instants et les structures de régions ou d'intervalles. D'une part les axiomatisations de structures d'entités étendues sont souvent faites avec en arrière pensée l'équivalence d'une structure sous-jacente d'entités ponctuelles qui forme le modèle de ces structures (ne serait-ce que parce que les structures ponctuelles ont nourri notre éducation mathématique et physique). Expliciter le lien est un moyen d'indiquer les modèles que l'on représente d'une autre façon ; c'est ce que signifient les isomorphismes entre structures montrés via des "théorèmes de représentation" [van Benthem, 1983]. Il est donc important de montrer comment on peut passer d'un type de représentation à un autre. La construction d'entités étendues à partir d'entités ponctuelles est généralement évidente, nous la verrons en premier avant de passer aux constructions moins connues qui font le chemin inverse.

Des points vers les intervalles

Soit une structure d'instants <math> I =\langle T, < \rangle</math>. La relation <math><</math> est une relation d'ordre sur <math>T</math>, donc irréflexive et transitive. On peut construire une structure d'intervalles de façon simple à partir de la structure de points : soit <math>I</math>, l'ensemble des ensembles d'instants construits sur <math>T</math>. On définit les deux relations suivantes, <math>\forall i\in I, \forall j\in I</math> :

• <math>i\sqsubseteq j \; \equiv \; \forall t \; (t\in i \rightarrow t\in j)</math>
• <math> i < j \; \equiv \; \forall t\in i, \; \forall t'\in j \; \;

\; t<t'</math>

et la structure résultante <math> T=\langle I, \sqsubseteq, < \rangle</math> est une structure d'intervalles, au sens de la section \resec:struct-base-su. On a alors une correspondance entre les propriétés des deux structures, si on se restreint à des intervalles non nuls et convexes, donc si on a :

• <math> \forall I \exists t \in I</math>
• <math> \forall t_1, t_2, t_3 (t_1\in I, t_2 \in I \land t_1<t_3<t_2)\rightarrow t_3\in I </math>

La relation <math><</math> entre intervalles est bien un ordre, la relation <math>\sqsubseteq</math> est réflexive, antisymétrique et transitive, et vérifie les propriétés suivantes : incompatibilité avec <math><</math>, existence de l'union et de l'intersection, orientation, liberté et liberté2, atomicité, monotonie, convexité, et ordre sur l'union.

Pour retrouver une structure similaire à la théorie de Allen, il faut imposer d'autres propriétés aux intervalles: ils doivent être bornés, donc définis par deux points extrémités orientés, et on définit alors la rencontre comme le "partage" d'une extrémité (la fin du premier intervalle et le début du second).

Des intervalles vers les points

La traduction précédente est assez naturelle, alors que le sens inverse l'est beaucoup moins, tant l'idée que le point est l'élément primitif de tout système du temps et de l'espace est ancrée dans nos conceptions. On doit pourtant à Russell et Wiener [Russell, 1914, Wiener, 1914] la construction de "points" comme ensemble d'intervalles, ceux-ci étant les structures primitives considérées. Russell considère les points comme ensembles d'intervalles convergents (le point est la limite d'une telle suite). Partant de l'idée que le point est une abstraction représentant l'élément minimum d'une représentation on peut considérer qu'un point dans une structure d'intervalles est un élément indécomposable, ce qui peut correspondre à un intervalle atomique par exemple. Pour recouvrer la notion générale même en l'absence d'intervalles atomiques, on peut construire les points comme des ensembles d'intervalles se recouvrant deux à deux. La structure utilisée correspondant à ces ensembles d'intervalles est celle d'un ultra-filtre . Un filtre <math>U</math> est un ensemble non vide de parties d'un ensemble <math> F</math> ayant les propriétés suivantes :

• <math>\forall A \in U \; \forall B \in U \; A\cap B \in

U</math>

• <math> \forall A \in U \; A\subset B \rightarrow B \in U </math> (on a donc <math> F\in U</math>).

Un ultra-filtre ou filtre maximal <math> U_1</math> est un filtre qui est maximal par rapport aux propriétés ci-dessus : si <math> U_2</math> est un filtre et <math> U_1\subseteq U_2 </math> alors <math> U_1=U_2 </math>

Sur une structure d'intervalles temporels <math =\langle I,\subseteq,<\rangle</math>, où <math>\sigma</math> désigne le recouvrement on peut définir des ultra-filtres de la façon suivante : <math>t</math> est un ultra-filtre si

• <math>\forall u\in t \; \forall v \in t \quad u\sigma v</math> et

l'intersection <math>u\cap v</math> appartient à <math>t</math>

• <math>\forall u\in t \; \; (u\subseteq v\rightarrow v\in t)</math>
• <math>t</math> est maximal

On peut alors définir une relation d'ordre sur les ultra-filtres de la façon suivante :

<math> t_1 << t_2 \; \equiv \; \; \exists u\in t_1 \; \exists v \in t_2 \quad u<v </math>

Cette relation est en effet trivialement irréflexive et transitive (par la transitivité de <math><</math>). On peut donc construire une structure d'instants <math>I=\langle T,<<\rangle</math> où <math>T</math> est l'ensemble des ultra-filtres construits sur <math> T</math, et <math><<</math> la relation définie ci-dessus. Cette dernière hérite de plus de certaines propriétés de <math><</math> ; ces liens sont étudiés précisément dans [van Benthem, 1983] et nous ne nous étendrons pas sur toutes les axiomatisations possibles. Il est cependant très important de voir à quelle condition on peut prétendre avoir une structure de points "équivalents" à la structure d'intervalles de départ. Pour cela on voit que l'on peut définir un intervalle comme ensemble des instants construits par ultra-filtres à partir de lui-même. Nous noterons cette opération comme suit :

• <math>u^*=\{ \; t \; | \; \; u\in t \; \}</math>

Soit <math>T^*</math> l'ensemble des intervalles construits de cette manière à partir des ultra-filtres de <math>T</math>, <math>\sqsubseteq</math> l'inclusion sur <math>T^*</math>, et <math><</math> l'ordre sur les intervalles induits par <math><<</math>\footnotDe la même façon qu'au paragraphe "Des points vers les intervalles" On note alors <math>T'^*=\langle T^*,\sqsubseteq,<\rangle</math> (note : cette construction retourne la définition classique d'un intervalle comme l'ensemble des points qu'il contient en ensemble des points le contenant). On peut parler d'isomorphisme de structure entre <math>T</math> et <math>T'^*</math> si les conditions suivantes sont vérifiées (cf. [van Benthem, 1983] ou [Landman, 1991]) :

• la fonction <math>f</math> définie par <math>f(u)=u^*</math> est bijective
• <math>u<v</math> si et seulement si <math>u^*<v^*</math>
• <math> u\subseteq v</math> si et seulement si <math>u^*\sqsubseteq v^*</math>

Il y a alors effectivement isomorphisme si la structure d'intervalles satisfait les propriétés de monotonicité, de conjonction (l'existence de l'intersection), de convexité, et les axiomes de liberté 1 et 2, pour les relations d'ordre partiel strict <math><</math> et d'ordre partiel <math>\subseteq</math>.

Les points dans la théorie d'Allen

Allen et Hayes ont indiqué dans [Allen & Hayes, 1989] une façon de construire une structure de points à partir de leur structure d'intervalle. La construction par ultra-filtre ne peut suffire dans la mesure où l'on veut introduire l'ensemble des lieux de contact entre intervalle mis en relation par la relation <math>meet</math>. Les points sont alors définis comme des classes d'équivalence de paires d'intervalles reliées par la relation <math>meet</math>. Si <math>a</math> est un point :

• <math>\forall \langle i,j \rangle \in a \; \forall k,l \; ((k||j \land

i||l)\rightarrow \langle k,l \rangle \in a)</math>

• <math>\forall \langle i_1,j_1 \rangle \in a \; \forall \langle i_2,j_2

\rangle \in a \quad (i_1||j_2 \land i_2||j_1)</math>

Cette construction garantit que les points sont des classes d'équivalence grâce à l'unicité des points de rencontre d'intervalles. Cette construction ne considère que les points de contact entre intervalles. Au cas où il existe des chaînes infinies d'intervalles inclus les uns dans les autres cette construction laisse de côté la limite éventuelle d'un telle série, et on ne retrouvera pas une structure de points équivalente (il manquera ce point limite).

Références

[Allen et Ferguson, 1994] J.F. Allen et G. Ferguson. Actions and events in interval temporal logic. Technical Report 521, The University of Rochester, Computer Science Dept., 1994.

[Allen et Hayes, 1989] J. Allen et P. Hayes. Moments and points in an interval-based temporal logic. Computationnal Intelligence, 5(4) :225-238, 1989.

[Allen, 1984] J. Allen. Towards a general theory of action and time. Arti\ufb01cial Intelligence, 23 :123-154, 1984.

[Davidson, 1967] D. Davidson. The logical form of action sentences. In The Logic of Decision and Action, éditeur N. Rescher. University of Pittsburgh Press, 1967.

[Galton, 1995] A. Galton. Time and change for IA. In Logics for Epistemic and Temporal Reasoning, éditeur Gabbay, volume 4 de Handbook of Logics for AI and Logic Programming. Oxford University Press, 1995.

[Hamblin, 1971] C.L. Hamblin. Instants and intervals. Studium Generale, 24 :127-134, 1971.

[Kamp, 1979] H. Kamp. Events, instants and temporal reference. In Meaning, use and interpretation of language, éditeur Von Stechow Bäuerle, Egli, pages 376-417. de Gruyter, Berlin, 1979.

[Landman, 1991] F. Landman. Structures for Semantics. Kluwer, Dordrecht, 1991.

[Russell, 1914] Bertrand Russell. Our Knowledge of the External World. Routledge, London and New York, 1914.

[van Benthem, 1983] J. van Benthem. The logic of time. Reidel, Dordrecht, 1983.

[van Benthem, 1995] J. van Benthem. Temporal logic. In Logics for Epistemic and Temporal Reasoning, éditeur Gabbay, volume 4 de Handbook of Logics for AI and Logic Programming. Oxford University Press, 1995.

[Wiener, 1914] N. Wiener. A contribution to the theory of relative position. Proceedings of the Cambridge Philosophical Society, (17) :441-449, 1914.

Relecture en cours Les commentaires des relecteurs de cet article n'ont pas encore été intégrés. Il n'est peut-être donc pas dans sa forme définitive.