1 Introduction et motivation
Les logiques modales, dont les logiques temporelles sont des cas
particuliers, ont été proposées au début du vingtième
siècle par Clarence Lewis [Lew18]. Lewis n'était pas
satisfait de l'implication matérielle de la logique classique, et a
exploré une autre variété de logiques, où un nouvel
opérateur 
(``box'') est utilisé. Au départ, 
F
signifiait ``il est nécessaire que F'', et ¬
¬F,
aussi noté àF, signifiait ``il est possible que
F''. Lewis a ensuite proposé plusieurs ensembles de règles
pour les nouveaux connecteurs, et a discuté leurs significations
intuitives possibles.
Certaines de ces interprétations relèvent de réflexions
philosophiques sur la notion de conséquence et d'implication.
Considérer par exemple la formule (
F)Þ F. Si nous
interprétons 
F comme ``A sait que F est vraie'',
alors 
F Þ F signifie ``Si A sait que F est
vraie, alors F est vraie''; si ceci est le cas pour tout F,
cette formule affirme que A ne fait pas d'erreur. La logique qui en
résulte est appelée une logique de la connaissance. Ces logiques
peuvent aussi modéliser le raisonnement temporel : si 
F
signifie ``dans tous les futurs possibles, F'' (ou ``à partir
de maintenant, F''), alors (
F)Þ F dit que chaque
fois que F est vraie à partir d'un certain instant, alors elle
est vraie à cet instant précis aussi.
Dans ces interprétations, la formule FÞ
F n'est pas
vraie en général. Par exemple, dans l'interprétation
temporelle, FÞ
F signifie que si F est vraie à
un instant, alors elle restera toujours vraie après coup.
D'un autre côté, si nous avons prouvé F dans un système
modal, nous pourrons en déduire 
F. Intuitivement, si
F est prouvée, alors elle est toujours vraie. (C'est
la raison pour laquelle 
se lit ``nécessairement''.)
Autrement dit, si F est prouvée, alors elle est vraie à tout
instant, donc dans tous les futurs de tous les instants. Le fait
surprenant que l'on puisse déduire 
F de F, mais que
FÞ
F ne soit pas valide veut dire que l'implication
Þ et la conséquence |- ne coïncideront pas dans les
logiques modales; autrement dit, le théorème de la déduction ne
sera pas vérifié.
Pourquoi nous intéressons-nous à de telles logiques ? Laissant de
côté les considérations philosophiques, les logiques modales et
en particulier les logiques temporelles ont fait leurs preuves en tant
que langages suffisamment expressifs, tout en restant décidables,
pour exprimer des spécifications de modèles de calcul
séquentiels et parallèles, et grâce auxquels la vérification
d'une réalisation informatique par rapport à une spécification
est décidable par des techniques simples à base d'automates. D'un
point de vue logique, il est aussi intéressant d'explorer les
rapports entre les logiques modales et non modales (comme la logique
intuitionniste), pour mieux comprendre ce qui les rapproche.
Finalement, les logiques modales ont été utilisées dans la
formalisation des logiques non monotones, dont le but est de
modéliser des affirmations comme ``en général, F est
vraie'' qui puissent survivre à la découverte de cas particuliers
où F ne serait pas vraie.
Nous étudions maintenant ces aspects des logiques modales. Nous
étudions d'abord la logique modale S4 en
section 2, et illustrons sur cet exemple la
formalisation des logiques non monotones. Nous choisissons S4 parce
qu'elle est une des logiques modales les plus simples et les plus
intéressantes, et aussi parce que c'est une logique temporelle.
Ceci nous mènera naturellement à l'étude de logiques temporelles
servant à la spécification de propriétés de systèmes de
transitions en section 3, et de méthodes de
vérification qu'un système de transitions satisfait une
spécification dans ces logiques, la vérification de
modèle (en anglais, ``model-checking'').
Le lecteur qui s'intéresse aux aspects logiques des logiques modales
est prié de consulter [Che80] ou
[HC68, HC84].
[Eme90, KT90] sont des textes sur les
logiques temporelles et la vérification de modèle.