Corrigé X-ENS 2026 Informatique C MPI — Partie II (Q7 à Q12) : Ultime invariance, parcours en profondeur imbriqués

Q7. Lecture de la figure : $s_0\stackrel{\alpha }{\to }{s}_1$, $s_0\stackrel{\beta }{\to }{s}_2$, $s_1\stackrel{\beta }{\to }{s}_1$, $s_1\stackrel{\alpha }{\to }{s}_3$, $s_2\stackrel{\alpha }{\to }{s}_2$, $s_2\stackrel{\beta }{\to }{s}_3$, $s_3\stackrel{\alpha }{\to }{s}_4$, $s_3\stackrel{\beta }{\to }{s}_5$, $s_4\stackrel{\alpha }{\to }{s}_6$, $s_5\stackrel{\alpha }{\to }{s}_5$, $s_5\stackrel{\beta }{\to }{s}_6$, $s_6\stackrel{\alpha }{\to }{s}_4$. Aucun état n'est terminal, donc toute exécution finie se prolonge en une exécution infinie : $s\models {\Phi }^{\omega }$ si et seulement si tous les états accessibles depuis $s$ (lui compris) sont dans $\Phi$.

• $s\models {\Phi }^{\omega }$ pour $s\in \{s_4,s_5,s_6\}$ : depuis $s_4$ ou $s_6$ on n'atteint que $\{s_4,s_6\}$, depuis $s_5$ que $\{s_5,s_6,s_4\}$, tous dans $\Phi$. En revanche $s_0,s_1,s_3\notin \Phi$, et $s_2$ atteint $s_3\notin \Phi$ (trace $s_2{s}_3{s}_4{s}_6{s}_4\dots$).
• $s\models \mathsf{EA}\Phi$ pour $s\in \{s_2,s_3,s_4,s_5,s_6\}$. Depuis $s_0$ ou $s_1$, l'exécution qui boucle sur $s_1$ par $\beta$ a pour trace $\dots s_1{s}_1{s}_1\dots$, jamais dans $\Phi$ à partir d'un rang : $s_0,s_1/\models \mathsf{EA}\Phi$. Depuis $s_3$, on passe en $s_4$ ou $s_5$, et l'on n'en sort plus de $\{s_4,s_5,s_6\}\subseteq \Phi$ : toute trace est dans $\Phi$ dès le rang $1$. Depuis $s_2$, soit on boucle indéfiniment sur $s_2\in \Phi$, soit on passe par $s_3$ une seule fois puis on reste dans $\Phi$. Les autres sont déjà dans ${\Phi }^{\omega }\subseteq \mathsf{EA}\Phi$.

C'est conforme à Q8 : le seul état hors de $\Phi$ qui fait un cycle est $s_1$ ($s_0$ n'a pas d'arc entrant, $s_3$ ne revient jamais sur lui-même), accessible depuis $s_0$ et $s_1$ seulement. Exécuté : verify (avec l'outer_iter de Q10) rend true exactement pour $s_2,\dots ,s_6$.

Q8. ($\Leftarrow$) Soit $s\stackrel{u}{\to }{s}^{\prime }$ et $s^{\prime }\stackrel{v}{\to }{s}^{\prime }$ avec $|v|⩾1$ et $s^{\prime }\notin \Phi$. L'exécution infinie $s\stackrel{u}{\to }{s}^{\prime }\stackrel{v}{\to }{s}^{\prime }\stackrel{v}{\to }{s}^{\prime }\cdots$ passe par $s^{\prime }$ à une infinité de positions : pour tout $i$, il existe $j⩾i$ avec $w_j=s^{\prime }\notin \Phi$. Sa trace n'est pas dans $\mathsf{EA}\Phi$, donc $s/\models \mathsf{EA}\Phi$.

($\Rightarrow$) Si $s/\models \mathsf{EA}\Phi$, une exécution infinie $\pi$ issue de $s$ a une trace $w\notin \mathsf{EA}\Phi$ : pour tout $i$ il existe $j⩾i$ avec $w_j\notin \Phi$. L'ensemble $J=\{j\mid w_j\notin \Phi \}$ est donc infini. Comme $S$ est fini, par le principe des tiroirs, deux positions $i<j$ de $J$ portent le même état $s^{\prime }=w_i=w_j\notin \Phi$. Le préfixe de $\pi$ jusqu'à la position $i$ est une exécution de $s$ à $s^{\prime }$ ; le morceau entre $i$ et $j$ est une exécution de $s^{\prime }$ à $s^{\prime }$, de longueur $j-i⩾1$.

Q9. L'énumération est l'ordre de fin de visite. Pour chaque état $x$ de l'arbre, notons $d(x)$ et $f(x)$ les instants de début et de fin de sa visite (appel récursif sur $x$). La visite de $x$ contient celles de ses fils, lancées l'une après l'autre dans l'ordre de visite : les intervalles $[d(x),f(x)]$ sont emboîtés ou disjoints, emboîtés exactement quand l'un est ancêtre de l'autre (propriété des parenthèses). L'ordre des $f$ place chaque nœud après ses descendants (a) et le sous-arbre d'un frère visité plus tôt avant celui d'un frère visité plus tard (b) ; comme (a) et (b) déterminent entièrement l'énumération, « $x$ précède $y$ » équivaut à $f(x)<f(y)$.