Exercices sur les automates d'arbres: étendre celui pour CTL pour la logique CTL étendue avec l'opérateur "EGF phi" (il existe un chemin le long duquel phi apparait infiniment souvent). Idem avec l'opérateur "EG2 phi" défini par "il existe un chemin où phi est vraie tous les états pairs (ie situés à une distance paire depuis l'état courant)".