Lec 27: CTL: Syntax and Semantics

Ce cours, le vingt-septième d’une série sur les méthodes formelles pour la vérification de systèmes, se concentre sur la définition formelle de la syntaxe et de la sémantique de la logique temporelle arborescente CTL. Le professeur Chandan Karfa commence par rappeler la syntaxe : les propositions atomiques, les opérateurs booléens, les opérateurs temporels (X, G, F, U) et les quantificateurs de chemin (A, E). Il insiste sur la priorité des opérateurs et l’associativité, recommandant l’utilisation de parenthèses. Ensuite, il définit la sémantique en se basant sur une structure de Kripke (ou système de transition), où chaque état est étiqueté par des propositions atomiques. Il explique formellement la satisfaction pour chaque opérateur : EX, AX, EG, AG, EF, AF, EU, AU, en précisant qu’il s’agit de chemins dans un arbre de branchement. Il illustre ces définitions avec un exemple concret : un système de transition avec trois états (S0, S1, S2) et des propositions P, Q, R. Il vérifie plusieurs formules, comme EX(P∧Q), ¬AX(P∧R), EF(P∧R), EG(R), AF(R), A(P∧Q U R), et une formule plus complexe impliquant AG et EF. Il conclut en résumant les acquis : la syntaxe et la sémantique de CTL, et la vérification de propriétés sur un modèle.