UNIVERSITE DE LA MANOUBA
Mati re : Logiques non classiques
----- -----
ECOLE NATIONALE DES SCIENCES DE L'INFORMATIQUE
Classes : II.3-ISID
A-U : 2013-2014
TD1-Logiques PLTL et CTL
Exercices 1.
1) Construire un automate fini (de B chi) qui accepte (p U q), Expliquer et donner une
expression r guli re associ e
2) Construire un automate de B chi reconnaissant p
Advertisement
3) D finir s mantiquement la formule (p q)
4) Prouver que la formule
((CoteDt2=g ' O(CoteDt2=d)) Dt2=o)
est quivalente la formule
((Dt2=l ' CoteDt2=g) O(CoteDt2=d)).
Exercice 2.
1)
Les quivalences suivantes sont-elles satisfaites, si oui donner une d monstration,
si non donner un contre exemple
2)
3)
Advertisement
Sachant que p q est labr viation de (p
Montrer que p q, q r |-- p r
Montrer la r gle d riv e suivante
q)
p
--------
p
1/2
Exercice 3.
On consid re un tunnel de montagne qui ne permet le passage que dun seul train la fois.
Deux trains circulent sur cette ligne.
Advertisement
Afin dassurer la s curit des voyageurs, chaque train peut
changer des signaux avec lordinateur qui assure le trafic dans
le tunnel (le m diateur). Ces signaux sont de trois types :
- attente : le train veut traverser le tunnel et attend une
autorisation,
- entr e : le train obtient lautorisation dentrer dans le tunnel,
- sortie : le train sort du tunnel.
Chaque signal est index par le num ro du train concern . Les signaux mis sont not s !x,
les signaux re us ?x.
1) Mod liser le comportement des deux trains par des automates
2) Mod liser le controleur des trains
3) Donner un mod le du syst me composite
Advertisement
4) Exprimer en CTL les propri t s suivantes :
- Les deux trains ne traversent jamais en m me temps le tunnel (s ret de
lacc s).
- Un train en attente finit toujours par traverser le tunnel (Vivacit ).
- Un train qui est sorti peut toujours se mettre en attente (non-blockage).
5) V rifier la premi re propri t sur lautomate qui d crit le syst me global
2/2