TD 11 : Automates pondérés, logique MSO et AFP

Quelques exemples

\[\Vert q \Vert ≝ \sum\limits_{ C∈C_q \text{ chemins partant de } q} \Vert C \Vert\]

pour $w∈𝛴^\ast$

\[⟦𝒜⟧(w) = \sum\limits_{ C∈ C_w \text{ chemins lisant } w} \Vert C \Vert\] \[\vert C_w \vert = \vert Q \vert^{\vert w \vert +1}\]

(l’automate pondéré est complet car $𝜇$ est une fonction totale)

Exemples

  digraph {
    rankdir=LR;
    q_2[shape=doublecircle]
    subgraph cluster_0{
      label = "𝒜"
      q_0, q_1, q_2;
    }
    q_0 -> q_0[label="a, b"];
    q_0 -> q_1[label="a"];
    q_1 -> q_2[label="b"];
    q_2 -> q_2[label="a, b"];
  }

\[L(𝒜) = 𝛴^\ast ab 𝛴\ast \\ B ≝ ⟨ \lbrace 0,1 \rbrace, ∨, ∧, 0, 1 ⟩\]

On veut un AFP $𝒜_{AFP}$ sur $B$ tq

\[⟦𝒜_{AFP}⟧(w) ≝ \begin{cases} 1 \text{ si } w∈L(𝒜) \\ 0 \text{ sinon} \end{cases}\] \[𝜆(q) ≝ \begin{cases} 1 \text{ si } q \text{ est initial} \\ 0 \text{ sinon} \end{cases}\] \[𝛾(q) ≝ \begin{cases} 1 \text{ si } q \text{ est final} \\ 0 \text{ sinon} \end{cases}\] \[𝜇(q, a, q') ≝ \begin{cases} 1 \text{ si } q ⟶^a_𝒜 q' \text{ est une transition de } 𝒜 \\ 0 \text{ sinon} \end{cases}\]

---

  digraph {
    rankdir=LR;
    q_2[shape=doublecircle]
    subgraph cluster_0{
      label = "𝒜"
      q_0, q_1, q_2;
    }
    q_0 -> q_0[label="a, b"];
    q_0 -> q_1[label="a"];
    q_1 -> q_2[label="b"];
    q_2 -> q_2[label="a, b"];
  }

\[L(𝒜) = 𝛴^\ast ab 𝛴\ast \\ S_𝛴 ≝ ⟨ ℙ(𝛴^\ast), ∪, \cdot, ∅, \lbrace 𝜀 \rbrace ⟩\]

On veut un AFP $𝒜_{AFP}$ sur $B$ tq

\[⟦𝒜_{AFP}⟧(w) ≝ \begin{cases} \lbrace w \rbrace \text{ si } w∈L(𝒜) \\ ∅ \text{ sinon} \end{cases}\] \[𝜆(q) ≝ \begin{cases} \lbrace 𝜀 \rbrace \text{ si } q \text{ est initial} \\ ∅ \text{ sinon} \end{cases}\] \[𝛾(q) ≝ \begin{cases} \lbrace 𝜀 \rbrace \text{ si } q \text{ est final} \\ ∅ \text{ sinon} \end{cases}\] \[𝜇(q, a, q') ≝ \begin{cases} \lbrace a \rbrace \text{ si } q ⟶^a_𝒜 q' \text{ est une transition de } 𝒜 \\ ∅ \text{ sinon} \end{cases}\]

---

• $⟨ℕ, \min, +⟩$
• $⟨ \lbrace 0, 1 \rbrace , ∨, ∧⟩$
• $⟨2^{𝛴^\ast}, ∪, \cdot⟩$
• $⟨[0, 1], +, \cdot⟩$

---

z := 10
x := y + z
if x+y ≤ 10:
  x := x+1
halt

  digraph {
    rankdir=TB;
    q_0 -> q_1[label="z := 10"];
    q_1 -> q_2[label="x := y + z"];
    q_2 -> q_3[label="x+y ≤ 10"];
    q_3 -> q_f[label="x := x+1"];
    q_2 -> q_f[label="x+y > 10"];
  }

⇓

  digraph {
    rankdir=TB;
    q_0 -> q_1[label="z := e(∅)"];
    q_1 -> q_2[label="x := e(y, z)"];
    q_2 -> q_3[label="if e(x, y)"];
    q_3 -> q_f[label="x := e(x)"];
    q_2 -> q_f[label="else e(x, y)"];
  }

---

\[MSO(𝛴, S ≝ ⟨A, +, ×, 0, 1⟩) ≝ 𝛼∈A \mid P_a(x) \mid x<y \mid x∈X \mid ¬ P_a(x) \mid ¬(x<y) \mid x∉X \mid 𝜑 ∧ 𝜑 \mid 𝜑 ∨ 𝜑\\ \mid ∃x : 𝜑 \mid ∃X : 𝜑 \mid ∀x : 𝜑 \mid ∀X : 𝜑\] \[⟦𝜑⟧_𝜈(w)\] \[⟦a⟧_𝜈(w) ≝ a\] \[⟦P_a(x)⟧_𝜈(w) ≝ \begin{cases} 1 \text{ si } w_{𝜈(x)} = a \\ 0 \text{ sinon} \end{cases}\] \[¬ ⟦P_a(x)⟧_𝜈(w) ≝ \begin{cases} 1 \text{ si } ⟦P_a(x)⟧_𝜈(w) = 0 \\ 0 \text{ sinon} \end{cases}\] \[⟦𝜑 ∧ 𝜓⟧_{𝜈}(w) ≝ ⟦𝜑⟧_{𝜈}(w) × ⟦𝜓⟧_{𝜈}(w)\] \[⟦𝜑 ∨ 𝜓⟧_{𝜈}(w) ≝ ⟦𝜑⟧_{𝜈}(w) + ⟦𝜓⟧_{𝜈}(w)\] \[⟦∃x : 𝜑⟧_{𝜈}(w) ≝ \sum\limits_{ i ≤ \vert w \vert } ⟦𝜑⟧_{𝜈[x \mapsto i]}(w)\] \[⟦∀x : 𝜑⟧_{𝜈}(w) ≝ \prod\limits_{ i ≤ \vert w \vert } ⟦𝜑⟧_{𝜈[x \mapsto i]}(w)\] \[⟦∃X : 𝜑⟧_{𝜈}(w) ≝ \sum\limits_{ x∈X } ⟦∃ x: 𝜑⟧_𝜈(w)\]

\(⟦∀X : 𝜑⟧_{𝜈}(w) ≝ \prod\limits_{ x∈X } ⟦∀ x: 𝜑⟧_𝜈(w)\) ___

\[⟦2 ∧ P_a(x)⟧_{𝜈(x)) = 1}(ab) ≝ 2 × 1 = 2\]

Dans $⟨ℕ, +, ×, 0, 1⟩$ :

\[⟦∃x : P_a(x)⟧ (w) ≝ \vert w \vert_a\]

Dans $𝛴 = \lbrace a, b \rbrace, ⟨2^{𝛴^\ast}, ∪, \cdot, ∅, \lbrace 𝜀 \rbrace⟩$ :

\[⟦∀x : (P_a(x) ∧ \lbrace a \rbrace) ∨ (P_b(x) ∧ \lbrace b \rbrace)⟧ (w) ≝ \lbrace w \rbrace\]