TD1 CTL

propriétés Booléennes à considérer

• prop1 = “J’aime le chocolat”
• prop2 = “J’aime le café”
• prop3 = “Je fais une thèse”

Exprimer en logique temporelle CTL (en utilisant prop1, prop2 et prop3) les phrases suivantes

• J’aime maintenant et pour toujours le café et le chocolat
  • votre réponse
• Je finirai toujours par aimer le chocolat
  • votre réponse
• Il est possible qu’un jour j’aime le café temporairement
  • votre réponse
• Si je fais une thèse je finirai par aimer le café
  • votre réponse
• Il est possible que je finisse par aimer le café pour toujours
  • votre réponse

TD2 CTL

Par groupe de 2, sur les exemples du cours, réfléchir à comment exprimer (avec GMEC et CTL) que

• “la transition T n’est jamais franchissable”
  • réponse
• “la transition T2 n’est jamais franchie avant T1”
  • réponse (un fichier xml du réseau modifié sera à rendre sur Moodle pour cette question)