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

EX 3

Logique temporelle :

⊤ ∣ p \in A P ∣ \neg 𝜑 ∣ 𝜑 \land 𝜑 ∣ X 𝜑 ∣ 𝜑 U 𝜑

$X$ : next
$U$ : until

(2^{A P})^{+} ∋ 𝜈, \underset{< | 𝜈 |}{\underset{⏟}{i}} ⊨ 𝜑

$F$ : finally
- $F 𝜑 ≝ ⊤ U 𝜑$
- $𝜑$ est vraie ultimement
$G$ : globally
- $G 𝜑 ≝ \neg F \neg 𝜑$
- $𝜑$ est vraie à tout moment

Ex : dans un programme

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

$\emptyset {r} \emptyset {s}$ et $\emptyset {r} {r} \emptyset {r, s}$ sont des modèles de $G (r ⟶ F s)$ , mais pas $\emptyset {r} \emptyset {r} \emptyset^{n}$

Pour $w \in 𝛴^{+}$ où $𝛴 ≝ 2^{A P}$

⟦ 𝜑 ⟧_{w} \in {0, 1}^{| w |}

Ex :

$𝜑 = F p$ , $A P = {p}$ , $𝛴 = {\emptyset, {p}}$

\begin{matrix} w = \emptyset \emptyset {p} \emptyset \emptyset \\ ⟹ ⟦ 𝜑 ⟧_{w} = 11100 \end{matrix}

1.

L (𝜑) = {w \in 𝛴^{+} ∣ w, 0 ⊨ 𝜑}

𝜑 = G (\neg p ⟶ X p) \land G (p ⟶ (X \neg p) \lor \neg X ⊤) \land \neg p

2.

Logique FO :

⊥ ∣ x < y ∣ \forall x . 𝜑 ∣ \neg 𝜑 ∣ 𝜑 \lor 𝜑 ∣ P_{a} (x)

w, i ⊨_{L T L} 𝜑 ⟺ w, {x \mapsto i} ⊨_{F O} S T_{x} (𝜑)

\begin{matrix} S T_{x} (⊤) = \neg ⊥ \\ S T_{x} (\underset{\in A p}{\underset{⏟}{p}}) = \underset{a \in {a \subseteq V a r (𝜑) ∣ q \in a}}{⋁} P_{a} (x) \\ S T_{x} (\neg 𝜑) = \neg S T_{x} (𝜑) \\ S T_{x} (𝜑 ⋆ 𝜓) = S T_{x} (𝜑) ⋆ S T_{x} (𝜓) \\ S T_{x} (X 𝜑) = \exists y . (x < y \land (\neg \exists z . (x < z \land z < y)) \land S T_{y} (𝜑)) \\ S T_{x} (𝜑_{1} U 𝜑_{2}) = \exists y . (x \leq y \land S T_{y} (𝜑_{2}) \land \forall z . (x \leq z \land z < y) ⟶ S T_{z} (𝜑_{1})) \end{matrix}

3.

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

Automate pour $⟦ p ⟧$ :

Automate pour $⟦ F p ⟧$ :

Automate pour $⟦ F p \land F q ⟧$ :

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.

S F (𝜑) = l’ensemble des sous-formules de 𝜑

$q \subseteq S F (𝜑)$ est cohérent si :

Si $𝜑_{1} \land 𝜑_{2} \in S F (𝜑)$ , alors :
$𝜑_{1} \land 𝜑_{2} \in q ssi 𝜑_{1} \in q et 𝜑_{2} \in q$
si $\neg 𝜑 \in S F (𝜑)$ , alors
$\neg 𝜑 \in q ssi 𝜑 \notin q$

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

𝒜_{𝜑} ≝ ⟨ C \cup {q_{0}}, 2^{A P}, {0, 1}, 𝜀, 𝜌, q_{0}, 𝛿 ⟩

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

q ⟶^{a / b} q^{'}

ssi

pour $p \in A P$ , $p \in q^{'} ssi p \in a$
$⊤ \in q^{'}$
si $X 𝜑_{1} \in S F (𝜑)$ , alors

𝜑_{1} \in q \neq q_{0} ssi X 𝜑_{1} \in q^{'}

NB : $𝜑_{1} U 𝜑_{2} = 𝜑_{2} \lor (𝜑_{1} \land X (𝜑_{1} U 𝜑_{2}))$

si $𝜑_{1} U 𝜑_{2} \in S F (𝜑)$ alors

𝜑_{1} U 𝜑_{2} \in q^{'} ssi (𝜑_{2} \in q^{'} ou (𝜑_{1} \in q^{'} \land 𝜑_{1} U 𝜑_{2} \in q)) \land q \neq q_{0}

$b = 1$ ssi $𝜑 \in q^{'}$

Taille de l’automate : $\leq 2^{| S F (𝜑) |} = 2^{| 𝜑 |}$

Automates d’arbres

$𝛴 = {a, b}$

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

𝒜 ≝ ⟨ Q, 𝛴, 𝛿, F ⟩

\begin{matrix} Q = {\underset{nombre pair}{\underset{⏟}{q_{0}}}, \underset{nombre impair}{\underset{⏟}{q_{1}}}} \\ F = {q_{c}} \end{matrix}

𝛿 ≝ {(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}), \dots}

Share on

Twitter Facebook Google+ LinkedIn

EX 3

1.

2.

3.

4.

Automates d’arbres

Share on

Leave a comment