TD 14 : Logique temporelle linéaire, Automates d’arbres

EX 3

Logique temporelle :

\[\top \mid p ∈ AP \mid ¬ 𝜑 \mid 𝜑 ∧ 𝜑 \mid X 𝜑 \mid 𝜑 U 𝜑\]
  • $X$ : next
  • $U$ : until
\[(2^{AP})^+ \ni 𝜈, \underbrace{i}_{< \vert 𝜈 \vert} \vDash 𝜑\]

  • $F$ : finally

    • $F \, 𝜑 ≝ \top U 𝜑$
    • $𝜑$ est vraie ultimement

  • $G$ : globally

    • $G \, 𝜑 ≝ ¬ F ¬ 𝜑$
    • $𝜑$ est vraie à tout moment

Ex : dans un programme

  • $r$ : requête arrivée
  • $s$ : requête satisfaite

$∅ \lbrace r \rbrace ∅ \lbrace s \rbrace$ et $∅ \lbrace r \rbrace \lbrace r \rbrace ∅ \lbrace r, s \rbrace$ sont des modèles de $G(r ⟶ F s)$, mais pas $∅ \lbrace r \rbrace ∅ \lbrace r \rbrace ∅^n$

Pour $w ∈ 𝛴^+$ où $𝛴 ≝ 2^{AP}$

\[⟦𝜑⟧_w ∈ \lbrace 0, 1 \rbrace^{\vert w \vert}\]

Ex :

$𝜑 = F p$, $AP = \lbrace p \rbrace$, $𝛴 = \lbrace ∅, \lbrace p \rbrace \rbrace$

\[w = ∅∅ \lbrace p \rbrace ∅ ∅ \\ ⟹ ⟦𝜑⟧_w = 11100\]

1.

\[L(𝜑) = \lbrace w ∈ 𝛴^+ \mid w, 0 \vDash 𝜑 \rbrace\] \[𝜑 = G(¬p ⟶ Xp) ∧ G(p ⟶ (X¬p)∨¬X\top) ∧ ¬p\]

2.

Logique FO :

\[\bot \mid x < y \mid ∀x. 𝜑 \mid ¬ 𝜑 \mid 𝜑 ∨ 𝜑 \mid P_a(x)\]
\[w, i \vDash_{LTL} 𝜑 ⟺ w, \lbrace x \mapsto i \rbrace \vDash_{FO} ST_x(𝜑)\] \[ST_x(\top) = ¬ \bot \\ ST_x(\underbrace{p}_{∈Ap}) = \bigvee\limits_{a ∈ \lbrace a ⊆ Var(𝜑) \mid q ∈ a \rbrace} P_a(x) \\ ST_x(¬ 𝜑) = ¬ ST_x(𝜑) \\ ST_x(𝜑 \star 𝜓) = ST_x(𝜑) \star ST_x(𝜓) \\ ST_x(X𝜑) = ∃y. (x<y ∧ (¬∃z. (x<z ∧ z<y)) ∧ ST_y(𝜑)) \\ ST_x(𝜑_1 U 𝜑_2) = ∃y. \, (x ≤ y ∧ ST_y(𝜑_2) ∧ ∀z. (x ≤ z ∧ z < y) ⟶ ST_z(𝜑_1))\]

3.

$f$ est co-séquentielle ssi $\widetilde{f}$ est séquentielle, où $\widetilde{f}(w) ≝ \widetilde{f(\widetilde{w})}$ (mots miroirs)

Automate pour $⟦p⟧$ :

  digraph {
    rankdir=LR;
    subgraph cluster_0{
      label = "⟦p⟧"
      q_0;
      b1, b2[style=invis];
    }
    b1 -> q_0[label="𝜀"];
    q_0 -> q_0[label="a / 1  si p∈a |  b / 0 si p ∉ b"];
    q_0 -> b2[label="𝜀"];
  }

Automate pour $⟦Fp⟧$ :

  digraph {
    rankdir=LR;
    subgraph cluster_0{
      label = "⟦Fp⟧"
      q_0; q_1;
      b1, b2, b3[style=invis];
    }
    b1 -> q_0[label="𝜀"];
    q_0 -> q_0[label="b / 0 si p ∉ b"];
    q_0 -> b2[label="𝜀"];
    q_0 -> q_1[label="a / 1  si p∈a"];
    q_1 -> q_1[label="x / 1"];
    q_1 -> b3[label="𝜀"];
  }

Automate pour $⟦Fp ∧ Fq⟧$ :

  digraph {
    rankdir=LR;
    subgraph cluster_0{
      label = "⟦Fp ∧ Fq⟧"
      q_0; q_1; q_2; q_3;
      b1, b2, b3, b4, b5[style=invis];
    }
    b1 -> q_0[label="𝜀"];
    q_0 -> q_0[label="b / 0 si p, q ∉ b"];
    q_0 -> b2[label="𝜀"];
    q_0 -> q_1[label="a / 1  si p∈a"];
    q_1 -> q_1[label="x / 1 si q∉x"];
    q_1 -> b3[label="𝜀"];
    q_0 -> q_2[label="a / 1  si q∈a"];
    q_2 -> q_2[label="x / 1 si p∉x"];
    q_2 -> b4[label="𝜀"];
    q_1 -> q_3[label="a / 1 si q ∈a"];
    q_2 -> q_3[label="a / 1 si p ∈a"];
    q_3 -> q_3[label="x / 1"];
    q_3 -> b5[label="𝜀"];
    q_0 -> q_3[label="a / 1 si p, q ∈a"];
  }

On note $E_𝜑$ l’ensemble des sous-formules de $𝜑$.

On peut, de manière algorithmique, construire l’automate :

  • ayant un état initial

  • tel que chaque état $q$ est indexé par le sous-ensemble de $E_𝜑$ des sous-formules vérifiées dans $q$

4.

Etant donnée $𝜑$ une formule LTL.

\[SF(𝜑) = \text{l'ensemble des sous-formules de } 𝜑\]
$q ⊆ SF(𝜑)$ est cohérent si :

  1. Si $𝜑_1 ∧ 𝜑_2 ∈ SF(𝜑)$ , alors :

    \[𝜑_1 ∧ 𝜑_2 ∈ q \text{ ssi } 𝜑_1 ∈ q \text{ et } 𝜑_2 ∈ q\]

  2. si $¬𝜑 ∈ SF(𝜑)$, alors

    \[¬𝜑 ∈ q \text{ ssi } 𝜑 ∉ q\]

Soit $C$ l’ensemble des états cohérents.

\[𝒜_𝜑 ≝ ⟨C ∪ \lbrace q_0 \rbrace, 2^{AP}, \lbrace 0, 1 \rbrace, 𝜀, 𝜌, q_0, 𝛿⟩\]

$𝛿$ (transitions avec sortie) satisfait les propriétés suivantes :

\[q ⟶^{a / b} q'\]

ssi

  1. pour $p∈AP$, \(p∈q' \text{ ssi } p ∈a\)

  2. $\top ∈ q’$

  3. si $X𝜑_1 ∈ SF(𝜑)$, alors

\[𝜑_1 ∈ q≠q_0 \text{ ssi } X𝜑_1 ∈ q'\]

NB : \(𝜑_1 U 𝜑_2 = 𝜑_2 ∨ (𝜑_1 ∧ X(𝜑_1 U 𝜑_2))\)

  1. si $𝜑_1 U 𝜑_2 ∈ SF(𝜑)$ alors
\[𝜑_1 U 𝜑_2 ∈ q' \text{ ssi } (𝜑_2 ∈ q' \text{ ou } (𝜑_1 ∈ q' ∧ 𝜑_1 U 𝜑_2 ∈ q)) ∧ q≠q_0\]
  1. $b=1$ ssi $𝜑 ∈ q’$

Taille de l’automate : \(≤ 2^{\vert SF(𝜑) \vert} = 2^{\vert 𝜑 \vert}\)

Automates d’arbres

$𝛴 = \lbrace a, b \rbrace$

Construire un automate d’arbres qui accepte les arbres binaires sur $𝛴$ avec un nombre pair de $a$.

\[𝒜 ≝ ⟨Q, 𝛴, 𝛿, F⟩\] \[Q = \lbrace \underbrace{q_0}_{\text{ nombre pair }}, \underbrace{q_1}_{\text{ nombre impair }} \rbrace \\ F = \lbrace q_c \rbrace\] \[𝛿 ≝ \lbrace (a, q_1), (b, q_0), (q_0, q_1, a, q_0), (q_0, q_1, b, q_1), (q_1, q_1, a, q_1), ⋯ \rbrace\]

Leave a comment