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).
Publicité
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 dune s quence contigu de q (au moins
1).
3. On doit avoir une s quence contigu de p (au moins 1), suivie dune s quence contigu de q (au moins
1), qui est suivie dune 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 innit de fois.
Exercice 3: Pour chacune des formules suivantes et le syst me de transition de la gure suivante,
Publicité
indiquer les tats o la formule est satisfaite. Dans le cas dune 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).
p, q
p, r
p
Publicité
q
p
q
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 dascenseur, un voyant indiquant si lascenseur a t appel de
l tage respectif, plus un bouton dappel. Proposer un nombre minimal de propositions atomiques et des
formules LTL permettant de sp cier les propri t s suivantes :
Une porte ne peut pas tre ouverte sans que lascenseur se trouve l tage respectif.
Publicité
Chaque appel sera servi dans lavenir.
Lascenseur doit revenir p riodiquement l tage 0.
Lorsquun appel du dernier tage est fait, lascenseur remonte tout de suite cet tage, sans sarr ter
en route.
Exercice 5: Construire un automate de B chi pour la formule p U 2 q.