Computer aided verification

Computer aided verification

Lecture 3:

LTL model-checking by translation to ω -automata

Sławomir Lasota University of Warsaw

Example:

φ = ¬G(p =⇒ X F q) 7→ Aφ =

// ?>=< 89:;

SS

p

// ?>=< 89:; 7654 0123

¬q

SS

LTL ⊆ ω-automata

– p. 2/45

Plan

– ω-automata

– LTL 7→ ω-automata – exponential blow-up

– LTL 7→ alternating ω-automata

ω -automata

– p. 4/45

ω -automata (BA)

Def.: ω-automaton (Büchi automaton) A = hΣ, S, Sinit, σ, F i – Σ finite input alphabet

– S finite set of states

– Sinit ⊆ S nonempty subset of initial states – σ ⊆ S × Σ × S transition relation

– F ⊆ S nonempty subset of accepting states

ω -automata (BA)

Def.: ω-automaton (Büchi automaton) A = hΣ, S, Sinit, σ, F i – Σ finite input alphabet

– S finite set of states

– Sinit ⊆ S nonempty subset of initial states – σ ⊆ S × Σ × S transition relation

– F ⊆ S nonempty subset of accepting states

A is deterministic when |Sinit| = 1 and ∀s, a. |σ(s, a)| ≤ 1.

– p. 5/45

ω -automata (BA)

Def.: ω-automaton (Büchi automaton) A = hΣ, S, Sinit, σ, F i – Σ finite input alphabet

– S finite set of states

– Sinit ⊆ S nonempty subset of initial states – σ ⊆ S × Σ × S transition relation

– F ⊆ S nonempty subset of accepting states

A is deterministic when |Sinit| = 1 and ∀s, a. |σ(s, a)| ≤ 1.

ω-words: w = a0 a1 a2 . . .

ω -automata (BA)

Def.: For w = a0 a1 a2 . . ., a run of an automaton A is r = s₀ s₁ s₂ . . . such that ∀i. (si, ai, si+1) ∈ σ.

– p. 6/45

ω -automata (BA)

Def.: For w = a0 a1 a2 . . ., a run of an automaton A is r = s₀ s₁ s₂ . . . such that ∀i. (si, ai, si+1) ∈ σ.

A run is accepting when si ∈ F for infinitely many i.

ω -automata (BA)

Def.: For w = a0 a1 a2 . . ., a run of an automaton A is r = s₀ s₁ s₂ . . . such that ∀i. (si, ai, si+1) ∈ σ.

A run is accepting when si ∈ F for infinitely many i.

Let inf(r) = {s ∈ S : s = si for infinitely many i}.

A run is accepting when inf(r) ∩ F 6= ∅.

– p. 6/45

ω -automata (BA)

Def.: For w = a0 a1 a2 . . ., a run of an automaton A is r = s₀ s₁ s₂ . . . such that ∀i. (si, ai, si+1) ∈ σ.

A run is accepting when si ∈ F for infinitely many i.

Let inf(r) = {s ∈ S : s = si for infinitely many i}.

A run is accepting when inf(r) ∩ F 6= ∅.

Lω(A) := {w ∈ Σ^ω : A has an accepting run for w}.

ω -automata (BA)

Def.: For w = a0 a1 a2 . . ., a run of an automaton A is r = s₀ s₁ s₂ . . . such that ∀i. (si, ai, si+1) ∈ σ.

A run is accepting when si ∈ F for infinitely many i.

Let inf(r) = {s ∈ S : s = si for infinitely many i}.

A run is accepting when inf(r) ∩ F 6= ∅.

Lω(A) := {w ∈ Σ^ω : A has an accepting run for w}.

Def.: A language is L ⊆ Σ^ω is ω-regular if L = Lω(A) for some A.

– p. 6/45

ω -automata (BA)

An accepting run looks like:

// 7654 0123 ,, 7654 0123 '&%$ !"#

BCD

@GA 88 ECD

@GF && XX FED ABC

Examples

Σ = {a, b}

infinitely often a (b^∗ a)^ω

7654 0123 

a

##

b

MM 7654 0123 '&%$ !"#

a,b

cc

– p. 8/45

Examples

Σ = {a, b}

infinitely often a (b^∗ a)^ω

7654 0123 

a

##

b

MM 7654 0123 '&%$ !"#

a,b

cc

odd(a) (a (a + b))^ω

7654 0123 

a

##7654 0123 '&%$ !"#

a,b

cc

Examples

Σ = {a, b}

infinitely often a (b^∗ a)^ω

7654 0123 

a

##

b

MM 7654 0123 '&%$ !"#

a,b

cc

odd(a) (a (a + b))^ω

7654 0123 

a

##7654 0123 '&%$ !"#

a,b

cc

LT L ( ω-automata

– p. 8/45

Exercise

– infinitely often a’s and b’s

– between any two consecutive a’s an even number of b’s

b^∗ (aa^∗ bb(bb)^∗)^ω

Exercise

– infinitely often a’s and b’s

– between any two consecutive a’s an even number of b’s

b^∗ (aa^∗ bb(bb)^∗)^ω

7654 0123

b

b

 oo

7654

0123 '&%$ !"#

** 7654 0123

b

]]

a

44 oo

Exercise

– infinitely often a’s and b’s

– between any two consecutive a’s an even number of b’s

b^∗ (aa^∗ bb(bb)^∗)^ω

7654 0123

b

b

 oo

7654

0123 '&%$ !"#

** 7654 0123

b

]]

44 oo

Exercise

– infinitely often a’s and b’s

– between any two consecutive a’s an even number of b’s

b^∗ (aa^∗ bb(bb)^∗)^ω

7654 0123

b

b

 oo

7654

0123 '&%$ !"#

** 7654 0123

b

]]

a

44 oo

and what about deterministic ?

7654 0123

b

 7654

0123 '&%$ !"#

**

b

66

7654 0123

b

]]

a

44 7654 0123

oo

b

44 oo

Exercise

– infinitely often a’s and b’s

– between any two consecutive a’s an even number of b’s

b^∗ (aa^∗ bb(bb)^∗)^ω

7654 0123

b

b

 oo

7654

0123 '&%$ !"#

** 7654 0123

b

]]

a

44 oo

and what about deterministic ?

7654 0123

b

 7654

0123 '&%$ !"#

**

b

66

7654 0123

b

]]

a

44 7654 0123

oo

b

44 oo

7654 0123

b



a



7654 0123 oo

7654

0123 '&%$ !"#

**

b

66

7654 0123

b

]]

44 7654 0123

oo 44 oo

Exercise

finitely often a (b + a)^∗b^ω

– p. 10/45

Exercise

finitely often a (b + a)^∗b^ω

// 7654 0123

b

//

a,b

7654 0123 '&%$ !"#

b

tt

Exercise

finitely often a (b + a)^∗b^ω

// 7654 0123

b

//

a,b

7654 0123 '&%$ !"#

b

tt

and what about deterministic ?

– p. 10/45

Determinisation?

– powerset construction does not work

No determinization!

Thm: (a + b)^∗b^ω is not accepted by a deterministic automaton.

– p. 12/45

No determinization!

Thm: (a + b)^∗b^ω is not accepted by a deterministic automaton.

Proof: Assume Lω(A) = (a + b)^∗b^ω, A deterministic.

No determinization!

Thm: (a + b)^∗b^ω is not accepted by a deterministic automaton.

Proof: Assume Lω(A) = (a + b)^∗b^ω, A deterministic.

w0 = b^ω. For some k0, σ(s0, b^k0) ∈ F .

– p. 12/45

No determinization!

Thm: (a + b)^∗b^ω is not accepted by a deterministic automaton.

Proof: Assume Lω(A) = (a + b)^∗b^ω, A deterministic.

w0 = b^ω. For some k0, σ(s0, b^k0) ∈ F .

w1 = b^k0ab^ω. For some k1, σ(s0, b^k0ab^k1) ∈ F . . . .

No determinization!

Thm: (a + b)^∗b^ω is not accepted by a deterministic automaton.

Proof: Assume Lω(A) = (a + b)^∗b^ω, A deterministic.

w0 = b^ω. For some k0, σ(s0, b^k0) ∈ F .

w1 = b^k0ab^ω. For some k1, σ(s0, b^k0ab^k1) ∈ F . . . .

∃i < j such that σ(s0, b^k0ab^k1 . . . ab^ki) = σ(s0, b^k0ab^k1 . . . ab^kj)

– p. 12/45

No determinization!

Thm: (a + b)^∗b^ω is not accepted by a deterministic automaton.

Proof: Assume Lω(A) = (a + b)^∗b^ω, A deterministic.

w0 = b^ω. For some k0, σ(s0, b^k0) ∈ F .

w1 = b^k0ab^ω. For some k1, σ(s0, b^k0ab^k1) ∈ F . . . .

∃i < j such that σ(s0, b^k0ab^k1 . . . ab^ki) = σ(s0, b^k0ab^k1 . . . ab^kj) Thus A accepts b^k0ab^k1 . . . ab^ki(a . . . ab^kj)^ω

contradiction!

Operations

Thm: ω-regular languages are closed under ∪, ∩ and complementation.

∨, ∧ and ¬

A1, A2 7→ A

(1) Lω(A) = Lω(A1) ∪ Lω(A2) (2) Lω(A) = Lω(A1) ∩ Lω(A2)

A 7→ ¯A

(3) Lω( ¯A) = Σ^ω \ Lω(A)

– p. 13/45

Intersection

(2) A1, A2 7→ A Lω(A) = Lω(A1) ∩ Lω(A2)

?

Intersection

(2) A1, A2 7→ A Lω(A) = Lω(A1) ∩ Lω(A2)

S = S1 × S2 × {1, 2}

Sinit = S1,init × S2,init × {1}

F = F1 × S2 × {1}

((s, t, i), a, (s^′, t^′, j)) ∈ σ ⇐⇒ (s, a, s^′) ∈ σ1, (t, a, t^′) ∈ σ2,

j =







2 if i = 1, s ∈ F1

1 if i = 2, t ∈ F2

i otherwise

– p. 15/45

Complementation?

(3) A 7→ ¯A Lω( ¯A) = Σ^ω \ Lω(A)

– no determinization

Complementation?

(3) A 7→ ¯A Lω( ¯A) = Σ^ω \ Lω(A)

– no determinization

– naive approach is not correct

// 7654 0123

b

//

a,b

7654 0123 '&%$ !"#

b

tt

// 7654 0123 '&%$ !"#

b

//

a,b

7654 0123

b

tt

– p. 16/45

Complementation

(3) A 7→ ¯A Lω( ¯A) = Σ^ω \ Lω(A)

– no determinization

Complementation

(3) A 7→ ¯A Lω( ¯A) = Σ^ω \ Lω(A)

– no determinization

– a complex construction

– p. 17/45

Complementation

(3) A 7→ ¯A Lω( ¯A) = Σ^ω \ Lω(A)

– no determinization

– a complex construction

– | ¯A| = 2^{O(n·log n)}, where n = |A|

Complementation

(3) A 7→ ¯A Lω( ¯A) = Σ^ω \ Lω(A)

– no determinization

– a complex construction

– | ¯A| = 2^{O(n·log n)}, where n = |A|

Moral: Better to avoid complementation

φ

✤ //

❴



¬φ

❴



✤

//

– p. 17/45

Complementation

Question: How complementation is done if A is deterministic?

Complementation

Question: How complementation is done if A is deterministic?

A

✤ //

F

✤ //

Lω( ¯A) = Σ^ω \ Lω(A) ?

– p. 18/45

Complementation

Question: How complementation is done if A is deterministic?

A

✤ //

F

✤ //

Lω( ¯A) = Σ^ω \ Lω(A) ? ^NO!

 

7654 0123

a

##

b

MM 7654 0123 '&%$ !"#

a,b

cc

7654 0123 '&%$ !"#

a

##

b

MM 7654 0123

a,b

cc

Complementation

Question: How complementation is done if A is deterministic?

A

✤ //

F

✤ //

Lω( ¯A) = Σ^ω \ Lω(A) ? ^NO!

 

7654 0123

a

##

b

MM 7654 0123 '&%$ !"#

a,b

cc

7654 0123 '&%$ !"#

a

##

b

MM 7654 0123

a,b

cc

co-Büchi: a run r = s0 s1 s2 . . . is accepting when si ∈ ¯F for almost all i (inf(r) ⊆ ¯F ).

– p. 18/45

Decision problems

problem for problem for complexity cost of

finite automata ω-automata algorithm

L(A) 6= ∅ Lω(A) 6= ∅ NLOGSPACE O(n)

L(A) = Σ^∗ Lω(A) = Σ^ω PSPACE 2^{O(n·log n)} L(A) ⊆ L(B) Lω(A) ⊆ Lω(B) PSPACE 2^{O(n·log n)}

L(AM) ⊆ L(Aφ)? vs L(AM) ∩ L(A¬φ) = ∅?

Decision problems

problem for problem for complexity cost of

finite automata ω-automata algorithm

L(A) 6= ∅ Lω(A) 6= ∅ NLOGSPACE O(n)

L(A) = Σ^∗ Lω(A) = Σ^ω PSPACE 2^{O(n·log n)} L(A) ⊆ L(B) Lω(A) ⊆ Lω(B) PSPACE 2^{O(n·log n)}

L(AM) ⊆ L(Aφ)? vs L(AM) ∩ L(A¬φ) = ∅?

Lasso

// 7654 0123 ,, 7654 0123 '&%$ !"#FED XX ABC

Thm: Lω(A) 6= ∅ iff A has a lasso.

– p. 19/45

LTL 7→ ω-automata

SPIN – examples

F G¬progress

// 7654 0123 BCD

@GA 88

¬progress

// 7654 0123 '&%$ !"#FED XX ABC

[Holzmann,Peled,Yannakakis 1996]

(co-Büchi ⊆ Büchi)

– p. 21/45

SPIN – examples (cont.)

SPIN’s doc

Generalized ω-automata (GBA)

– {F1, . . . , Fn} instead of F

– a run r is accepting when ∀i. inf(r) ∩ Fi 6= ∅

Question: Are generalized automata more expressive?

– p. 23/45

Generalized ω-automata (GBA)

– {F1, . . . , Fn} instead of F

– a run r is accepting when ∀i. inf(r) ∩ Fi 6= ∅

Question: Are generalized automata more expressive?

AF1...F_n 7→ AF

Lω(AF1...F_n) = Lω(AF)

Generalized ω-automata (GBA)

– {F1, . . . , Fn} instead of F

– a run r is accepting when ∀i. inf(r) ∩ Fi 6= ∅

Question: Are generalized automata more expressive?

AF1...F_n 7→ AF

Lω(AF1...F_n) = Lω(AF)

|AF | = O(|AF1,...,F_n| · n)

Lω(AF) ⊆ Lω(AF1) ∩ . . . ∩ Lω(AF_n)

– p. 23/45

LTL 7→ BA

– ^SPIN: LTL 7→ GBA 7→ BA

– LTL2BA: LTL 7→ ABA 7→ GBA’ 7→ BA

– On-the-fly verification

LTL 7→ GBA (1)

LTL⁺ :

φ := p | ¬p | φ1 ∧ φ2 | φ1 ∨ φ2 | X φ | φ1 Uφ2 | φ1 Rφ2 | true | false

Intuition: φ ≡ now(φ) ^∧_∨ later(φ)

φ U ψ ≡ ψ ∨ (φ ∧ X (φ U ψ)) φ R ψ ≡ ψ ∧ (φ ∨ X (φ R ψ))

(fixed points)

– p. 25/45

LTL 7→ GBA (2)

. . . do not think about tomorrow! :)

P = {¬p : p ∈ P }¯

α 7→ today(α) – positive boolean formula over facts P ∪ ¯P ∪ { X φ : φ . . .}

today facts P ∪ ¯P tomorrow facts { X φ : φ . . .}

today(α) = α, when α = p, ¬p, X β, true, false today(α ∨ β) = today(α) ∨ today(β)

today(α ∧ β) = today(α) ∧ today(β)

today(α U β) = today(β) ∨ (today(α) ∧ X (α U β)) today(α R β) = today(β) ∧ (today(α) ∨ X (α R β))

LTL 7→ GBA (3)

α 7→ today(α) 7→ dnf(α) ⊆ P(P ∪ ¯P ∪ { X φ : φ . . .})

today(α) ≡ dnf(α) ≡ ∨_X∈dnf(α) ∧ X

For example:

dnf(α) = {{α}}, when α = p, ¬p, X β dnf(α ∨ β) = dnf(α) ∪ dnf(β)

dnf(α ∧ β) = {X ∪ Y : X ∈ dnf(α), Y ∈ dnf(β)}

dnf(α U β) = dnf(β) ∪ dnf(α ∧ X (α U β)))

dnf(true) = {∅} ∧∅ ≡ true

dnf(false) = ∅ ∨∅ ≡ false

– p. 27/45

LTL 7→ GBA (4)

GBA Aφ = hΣ, S, Sinit, σ, F i:

– Σ = P(P )

– S = P(P ∪ ¯P ∪ { X φ : φ . . .}) – Sinit = dnf(φ)

– X −^A→ Y iff

– X ∩ P ⊆ A X and A non-contradictory today

– (X ∩ ¯P ) ∩ A = ∅

– Y ∈ dnf( ∧ {α | X α ∈ X}) possible tomorrow – F = ?

LTL 7→ GBA (example 1)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

φ ≡ b ∨ (¬a ∧ X φ)

– p. 29/45

LTL 7→ GBA (example 1)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

φ ≡ b ∨ (¬a ∧ X φ)

 

GFED

@ABC

//

@AB GFE

∅,{b}

 ?>=< 89:;

//?>=< 89:;

FED ABC

\\

LTL 7→ GBA (example 1)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

φ ≡ b ∨ (¬a ∧ X φ)

 

GFED

@ABC

//

@AB GFE

∅,{b}

 ?>=< 89:;

//?>=< 89:;

FED ABC

\\

 

GFED

@ABC

//

@AB GFE

¬a

 ?>=< 89:;

//?>=< 89:;

FED ABC

\\

– p. 29/45

LTL 7→ GBA (example 1)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

φ ≡ b ∨ (¬a ∧ X φ)

 

GFED

@ABC

//

@AB GFE

∅,{b}

 ?>=< 89:;

//?>=< 89:;

FED ABC

\\

 

GFED

@ABC

//

@AB GFE

¬a

 ?>=< 89:;

//?>=< 89:;

FED ABC

\\

F = ?

LTL 7→ GBA (example 1)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

φ ≡ b ∨ (¬a ∧ X φ)

 

GFED

@ABC

//

@AB GFE

¬a

 ?>=< 89:; /.-, ()*+

//?>=< 89:; /.-, ()*+

FED ABC

\\

F = {∅, {b}}

– p. 30/45

LTL 7→ GBA (F)

– {αi Uβi | i = 1, . . . , n} ⊆ subformulas(φ)

LTL 7→ GBA (F)

– {αi Uβi | i = 1, . . . , n} ⊆ subformulas(φ)

– S \ Fi = {X ∈ S | αi Uβi ∈ X ∧ βi ∈ X}/ , i = 1, . . . , n

– p. 31/45

LTL 7→ GBA (F)

– {αi Uβi | i = 1, . . . , n} ⊆ subformulas(φ)

– S \ Fi = {X ∈ S | αi Uβi ∈ X ∧ βi ∈ X}/ , i = 1, . . . , n – S \ Fi = {X ∈ S | αi Uβi ∈ cons(X) ∧ βi ∈ cons(X)}/

LTL 7→ GBA (F)

– {αi Uβi | i = 1, . . . , n} ⊆ subformulas(φ)

– S \ Fi = {X ∈ S | αi Uβi ∈ X ∧ βi ∈ X}/ , i = 1, . . . , n – S \ Fi = {X ∈ S | αi Uβi ∈ cons(X) ∧ βi ∈ cons(X)}/

X ⊆ cons(X)

α ∨ β ∈ cons(X) if α ∈ cons(X) α ∨ β ∈ cons(X) if β ∈ cons(X)

α ∧ β ∈ cons(X) if α ∈ cons(X) and β ∈ cons(X) α U β ∈ cons(X) if β ∨ (α ∧ X (α U β)) ∈ cons(X) α R β ∈ cons(X) if β ∧ (α ∨ X (α R β)) ∈ cons(X) true ∈ cons(X)

α U β ∈ cons(X) if β ∈ cons(X) or

α ∈ cons(X) and X (α U β)) ∈ X

– p. 31/45

LTL 7→ GBA (F)

– {αi Uβi | i = 1, . . . , n} ⊆ subformulas(φ)

– S \ Fi = {X ∈ S | αi Uβi ∈ X ∧ βi ∈ X}/ , i = 1, . . . , n – S \ Fi = {X ∈ S | αi Uβi ∈ cons(X) ∧ βi ∈ cons(X)}/

X ⊆ cons(X)

α ∨ β ∈ cons(X) if α ∈ cons(X) α ∨ β ∈ cons(X) if β ∈ cons(X)

α ∧ β ∈ cons(X) if α ∈ cons(X) and β ∈ cons(X) α U β ∈ cons(X) if β ∨ (α ∧ X (α U β)) ∈ cons(X) α R β ∈ cons(X) if β ∧ (α ∨ X (α R β)) ∈ cons(X) true ∈ cons(X)

α U β ∈ cons(X) if β ∈ cons(X) or

α ∈ cons(X) and X (α U β)) ∈ X

LTL 7→ GBA (example 1 cont.)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

 

GFED

@ABC

//

@AB GFE

¬a

 ?>=< 89:; /.-, ()*+

//?>=< 89:; /.-, ()*+

FED ABC

\\

S \ F = {X ∈ S | ¬a ∈ X ∧ X φ ∈ X ∧ b /∈ X}

Can automaton Aφ be smaller?

– p. 32/45

LTL 7→ GBA (example 1 cont.)

φ = ¬a U b S = P(a, ¬a, b, ¬b, X (¬a U b))

Σ = {∅, {a}, {b}, {a, b}}

 

GFED

@ABC

//

@AB GFE

¬a

 ?>=< 89:; /.-, ()*+

//?>=< 89:; /.-, ()*+

FED ABC

\\

S \ F = {X ∈ S | ¬a ∈ X ∧ X φ ∈ X ∧ b /∈ X}

Can automaton Aφ be smaller? ^YES!

// 7654 0123

//

BCD

@GA

¬a

88 7654 0123 '&%$ !"#

BCD

@GA

true

88

exponential blow-up

– p. 33/45

LTL 7→ GBA (example 2)

θ = ¬ G (q =⇒ F r) ≡ F (q ∧ G ¬r)

S = P(q, ¬q, r, ¬r, X ( F (q ∧ G ¬r)), X G ¬r) F = ?

dnf( F α) = dnf(α) ∨ X F α Fα ≡ α ∨ X F α

dnf( G α) = dnf(α ∧ X G α) Gα ≡ α ∧ X G α

dnf( F (q ∧ G ¬r)) = X F (q ∧ G ¬r) ∨ q ∧ ¬r ∧ X G ¬r

 

X F(q ∧ G ¬r) ^true

//

BCD

@GA

true

||

//

BCD

@GA

¬r

oo

LTL 7→ GBA (example 2)

θ = ¬( G F p =⇒ G (q =⇒ F r)) ≡ G F p ∧ F(q ∧ G ¬r)

dnf( F α) = dnf(α) ∨ X F α Fα ≡ α ∨ X F α

dnf( G α) = dnf(α ∧ X G α) Gα ≡ α ∧ X G α

dnf( F (q ∧ G ¬r)) = X F(q ∧ G ¬r) ∨ (q ∧ ¬r ∧ X G ¬r) dnf( G F p) = dnf((p ∨ X F p) ∧ X G F p) =

(p ∧ X G F p) ∨ ( X F p ∧ X G F p) dnf( G F p ∧ F(q ∧ G ¬r)) = . . . ∨ . . . ∨ . . . ∨ . . .

X F(q ∧ G ¬r), p, X G F p q, ¬r, X G ¬r, p, X G F p

X F(q ∧ G ¬r), X F p, X G F p q, ¬r, X G ¬r, X F p, X G F p

– p. 35/45

LTL 7→ GBA (example 2)

θn = ¬(( G F p1 ∧ . . . ∧ G F pn) =⇒ G (q =⇒ F r)) ≡

G Fp1 ∧ . . . ∧ G Fpn ∧ F(q ∧ G ¬r)

LTL 7→ GBA (example 3)

φn = p1 U(p2 U(. . . U pn) . . .)

?>=<

89:;

p1

// BCD

@GA

p1

>>

p1

p1

'' ?>=<

89:;

//

p2

:: BCD

@GA

p2

>>

?>=< 89:; 7654 0123

//

BCD

@GA

p_n

>> ?>=< 89:; /.-, ()*+

FED ABC

\\

θn = ¬ p1 U(p2 U(. . . U pn) . . .)

≡ ¬p1 R(¬p2 R(. . . R ¬pn) . . .)

φ R ψ ≡ ψ ∧ (φ ∨ X (φ R ψ))

– p. 37/45

LTL 7→ ABA

Alternation (ABA)

?>=<

89:;

?>=<

89:;

a

❃ ❃ ❃ ❃

❃

a

⑧ ⑧ ⑧ ⑧ ⑧ ??

⑧

GFED

@ABC

σ(p, a) = q ∨ q^′ (p, a, q), (p, a, q^′) ∈ σ

?>=<

89:;

?>=<

89:;

a



a

KK

and

GFED

@ABC

σ(p, a) = q ∧ q^′

—

Example transition: σ(p, a) = p1 ∨ p2 ∧ p3 (think of positive DNF) run = tree (dag) labeled with states

– p. 39/45

LTL 7→ ABA (1)

ABA Aφ = hΣ, S, Sinit, σ, F i:

– S = modal subformulas ( Xα, α U β, α R β), literals (p, ¬p), true, false – Sinit = φ !!!

– σ : S × Σ → Bool⁺(S)

σ(p, A) = accepts, if p ∈ A (otherwise rejects) σ(¬p, A) = accepts, if p /∈ A (otherwise rejects) σ(true, A) = accepts

σ(false, A) = rejects

σ( X α, A) = α !!!

σ(α U β, A) = σ(β, A) ∨ (σ(α, A) ∧ α U β) σ(α R β, A) = σ(β, A) ∧ (σ(α, A) ∨ α R β)

σ( F α, A) = σ(α, A) ∨ F α σ( G α, A) = σ(α, A) ∧ G α

LTL 7→ ABA (example)

φ = ¬( G F p =⇒ G (q =⇒ F r)) ≡ G Fp ∧ F (q ∧ G ¬r) σ(p, A) = accepts, if p ∈ A (otherwise rejects)

σ(¬p, A) = accepts, if p /∈ A (otherwise rejects) σ(true, A) = accepts

σ(false, A) = rejects

σ( F α, A) = σ(α, A) ∨ F α σ( G α, A) = σ(α, A) ∧ G α

σ( GF α, A) = (σ(α, A) ∨ F α) ∧ GF α

[Gastin,Oddoux 2001]

– p. 41/45

LTL 7→ ABA (example)

φ = ¬( G F p =⇒ G (q =⇒ F r)) ≡ G Fp ∧ F (q ∧ G ¬r)

[Gastin,Oddoux 2001]

LTL 7→ ABA (2)

ABA Aφ = hΣ, S, Sinit, σ, F i:

– S = modal subformulas ( Xα, α U β, α R β), literals (p, ¬p), true, false – Sinit = φ

– σ : S × Σ → Bool⁺(S) . . .

– F = {α R β}

– p. 43/45

LTL 7→ GBA vs LTL 7→ ABA

θn = ¬(( G F p1 ∧ . . . ∧ G F pn) =⇒ G (q =⇒ F r))

[Gastin,Oddoux 2001]

LTL and ω-automata

LTL

  //

linear alternating ω-automata

  //

– p. 45/45