TD3 - Introduction en logique temporelle linéaire
Exercice 1: Laquelle des formules suivantes est une tautologie :
C. Dima
1. 2 (cid:13) p ⇔ (cid:13) 2 p. 2. 2(p ⇒ q) ⇔ 2 p ⇒ 2 q. 3. (cid:13)(p U q) ⇒ ((cid:13) p) U((cid:13) q). 4. 2 3 p ⇒ 3 2 p. 5. 3 2 p ⇒ 2 3 p. 6. (2 p U 2 q) ⇒ 2(p U 2 q).
Exercice 2: Décrire en logique temporelle linéaire les propriétés suivantes :
1. p doit toujour précéder une apparition de q. 2. On doit avoir une séquence contiguë de p (au moins 1), suivie d’une séquence contiguë de q (au moins
Publicité
1).
3. On doit avoir une séquence contiguë de p (au moins 1), suivie d’une séquence contiguë de q (au moins
1), qui est suivie d’une séquence contiguë de r (au moins 1).
4. Toute apparition de p doit être suivie dans au plus 3 unités de temps par une apparition de q, et p doit
apparaître une infinité de fois.
Exercice 3: Pour chacune des formules suivantes et le système de transition de la figure suivante, indiquer les états où la formule est satisfaite. Dans le cas d’une formule non-satisfaite, donner une trace qui le prouve. 1. 2(p ∧ r → 2(q ∨ r)). 2. p U(p ∧ r). 3. 3(p ∧ (cid:7) q). 4. 2(r ⇒ p ∨ p ∨ (cid:13) p).
Publicité
p, q
p, r
p
q
p
q
Publicité
q, r
Exercice 4: Considérons un ascenseur pour un bâtiment à 4 étages (plus le rez-de-chaussée), pour lequel chaque étage possède une porte d’ascenseur, un voyant indiquant si l’ascenseur a été appelé de l’étage respectif, plus un bouton d’appel. Proposer un nombre minimal de propositions atomiques et des formules LTL permettant de spécifier les propriétés suivantes :
– Une porte ne peut pas être ouverte sans que l’ascenseur se trouve à l’étage respectif. – Chaque appel sera servi dans l’avenir. – L’ascenseur doit revenir périodiquement à l’étage 0. – Lorsqu’un appel du dernier étage est fait, l’ascenseur remonte tout de suite à cet étage, sans s’arrêter
en route.
Exercice 5: Construire un automate de Büchi pour la formule p U 2 q.