TD10 : Complexité : CTL

EX 1

  • neXt
  • Finally
  • Globally
  • Until
  • All

  • Exist

  • On commence par remarquer qu’on peut faire un parocurs en profondeur dans un graphe acyclique.

  • Étant donné une instance d’un circuit booléen : on peut parcourir l’ensemble des edges pour faire en sorte :

    • d’alterner les sommets $∧$ et $∨$
    • au premier niveau, de n’avoir que des $∧$
digraph {
rankdir = TB;
∧1[label="∧"];
∧2[label="∧"];
∧3[label="∧"];
∧4[label="∧"];


∨1[label="∨"];
∨2[label="∨"];

⋯1[label="⋯"];
⋯2[label="⋯"];

T -> ∧1;
F -> ∧2;
∧1 -> ⋯1;
∧2 -> ⋯2;
⋯1 -> ∨1;
⋯1 -> ∧4;

⋯2 -> ∨2;
⋯2 -> ∧3;

∨2 -> ∧3;
∨1 -> ∧4;
∧3 -> ∨;
∧4 -> ∨;

}

On remarque que :

  • un sommet $∧$ est vrai ⟶ AX pour ses fils
  • un sommet $∨$ est vrai ⟶ EX pour ses fils

On inverse le sens des arêtes, et on fait boucler T sur T, F sur F.

digraph {
rankdir = TB;
∧1[label="∧"];
∧2[label="∧"];
∧3[label="∧"];
∧4[label="∧"];


∨1[label="∨"];
∨2[label="∨"];

⋯1[label="⋯"];
⋯2[label="⋯"];

T -> T;
F -> F;

∧1 -> T;
∧2 -> F;
⋯1 -> ∧1;
⋯2 -> ∧2;
∨1 -> ⋯1;
∧4 -> ⋯1;

∨2 -> ⋯2;
∧3 -> ⋯2;

∧3 -> ∨2;
∧4 -> ∨1;
∨out -> ∧3;
∨out -> ∧4;

}
\[𝜑 = EX(AX(EX(⋯ True)))\]

où il y a $n$ imbriquations (avec $n$ la taille de l’entrée).

\[s=out \\ M,s \vDash 𝜓\]

Par induction :

Si $𝜓=AX(𝜑)$ OU $EX(𝜑)$

Hypothèse sur $h$ : tout sommet $s’$ de hauteur $h$ ($true ⟶^{h} s’$ ou $false ⟶^{h} s’$) vérifie

\[V(s')=true ⟺ M, s' \vDash 𝜓\]

avec $𝜓$ de la forme

\[\underbrace{EX(AX(⋯(true)))}_{h + 2k \text{ symboles, pour $k$ un entier}}\]

et $𝜓=AX(EX( ⋯ true))$

  • Si $h=0$ :

    \[M, true \vDash \underbrace{EX(AX(⋯(true)))}_{2k \text{ symboles, pour $k$ un entier}}=true\] \[M, false \vDash \underbrace{EX(AX(⋯(true)))}_{2k \text{ symboles, pour $k$ un entier}}=true\]

Si $h=2p$ vérifie l’hypothèse :

  • $h=2p+1$ ou $h=2p$ : vérifie l’hypothèse $h$.

    alors $V(s’) = true$ alors $V(s’) = ∧{s’’ \text{ successeur de} s’} V(s’’)$ alors $∀s’’, V(s’’) = true$, *i.e* $∀s’’, M, s’’ \vDash true$, *i.e* $M, s’’ \vDash \underbrace{EX(AX(⋯(true)))}{2p + 2k \text{ symboles}}=true$

    donc $M, s’ \vDash \underbrace{AX(EX(AX(⋯(true))))}_{2p + 2k +1 \text{ symboles}}=true$

$k’’$ tq profondeur($s’’$) + $2k’’ = 2p + 2k$

2.

\[M,s \vDash AX 𝜑 ⟺ M,s \vDash \lnot EX \lnot 𝜑\] \[M,s \vDash 𝜑 ∨ 𝜓 ⟺ M,s \vDash \lnot ( \lnot 𝜑 ∧ \lnot 𝜓)\] \[M,s \vDash AF 𝜑 ⟺ M,s \vDash \lnot (EG(\lnot 𝜑))\]
  • \[M,s \vDash AF 𝜑 ⟺ ∀𝜌, ∃i, M,𝜌(i) \vDash 𝜑 \\ ⟺ ∀𝜌, ∃i, M,𝜌(i) \vDash 𝜑 \\ ⟺ \lnot (∃𝜌, ∀i, M,𝜌(i) \vDash \lnot 𝜑) \\\]
\[M,s \vDash AG 𝜑 ⟺ M,s \vDash \lnot (EF(\lnot 𝜑))\] \[M,s \vDash EF 𝜑 ⟺ M,s \vDash E(\top U 𝜑))\] \[M,s \vDash A(𝜑U𝜓) ⟺ M,s \vDash \lnot E(𝜑U𝜓)\]
  • \[∀𝜌_s, ∃j, (𝜌(j) \vDash 𝜓) ∧ (∀i<j, 𝜌(i) \vDash 𝜑) \\ ≡ \lnot( ∃𝜌_s, ∀j, (𝜌(i) \vDash \lnot 𝜓) ∨ (∃i<j, 𝜌(i) \vDash \lnot 𝜑) )\]

3.

Soit $M=(S, ⟶, L)$.

S_model(𝜑) :

calcule l’ensemble $V$ tq $V=\lbrace s∈S \vert M,s \vDash 𝜑\rbrace$

S_model(𝜑):
    Si
        - 𝜑=⊤ : return S
        - 𝜑=⊥ : return ∅
        - 𝜑=p∈AP: return {s | p∈L(S)}
        - 𝜑 = 𝜓 ∨ 𝜋 : S_model(𝜓) ∪ S_model(𝜋)
        - 𝜑 = ¬ 𝜓 : return S\S_model(𝜓)
        - 𝜑 = EX 𝜓 : return ⟶^{-1}(S_model(𝜓))
        - 𝜑 = EG 𝜓 :
            S_model(𝜑) est le plus
            grand ensemble inclus dans
            S_model(𝜓) est stable par ⟶

            V ← S_model(𝜓)
            not_done ← true

            while(not_done):
                m ← |V|
                V ← V ∩ ⟶(V)
                if (m==|V|):
                    not_done ← false

On peut amélorier la complexité quadratique du dernier cas, avec un calcul de composante fortement connexes :

CC(V') ⟶ C_1, ⋯, C_k
V'' = union des C_i
return (⟶^{-1})^{*}(V'')∩V

Leave a comment