Informatique et Sciences du Numérique au lycée : un pas plus loin/LANGAGES/Logiques Temporelles et Vérification par modèles

La vérification par modèles (en anglais model checking) désigne une famille de techniques de vérification automatique de programmes (ou de systèmes), fondées sur la construction d'un modèle du programme (ou du système) adapté à la propriété étudiée. Ce modèle constitue une abstraction du programme en général sous la forme d'un automate et les propriétés sont exprimées par des formules d'une logique temporelle portant sur les états de l'automate.

Les différentes logiques temporelles sont des logiques mathématiques et plus précisément des logiques modales. La caractéristique commune de ces logiques, est l'ajout de modalités (c'est-à-dire des « transformeurs de prédicats ») permettant de donner une information sur le temps, par exemple, la formule $\phi U\psi$ peut se lire : « la formule $\phi$ est satisfaite jusqu'à ce que la formule $\psi$ le soit ».

Intuitivement, cela signifie que la notion de vérité dans ces logiques dépend de l'évolution du monde. C'est-à-dire qu'une proposition peut être, à un moment fausse, puis plus tard, devenir vraie.

Plusieurs logiques temporelles peuvent être décrites, en fonction des types de modalités de base qu'elles utilisent. On peut, par exemple, y exprimer simplement le fait qu'un événement dangereux ne doit pas arriver tant qu'une certaine condition de sécurité n'est pas satisfaite.