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

Leave a comment