CTL symbolic model-checking

Computer aided verification

Lecture 6:

CTL symbolic model-checking

Sławomir Lasota University of Warsaw

Idea of SMC: EF p

– Compute the set of all states satisfying EF p by iterating predecessor EX _.

– p. 2/65

Idea of SMC: EF p

– Compute the set of all states satisfying EF p by iterating predecessor EX _.

– Instead of enumerating all states individually...

compute symbolic description of the set

Symbolic model checking

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

– p. 3/65

Symbolic model checking

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

Plan:

– OBDDs

Symbolic model checking

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

Plan:

– OBDDs

– Boolean encoding

– p. 3/65

Symbolic model checking

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

Plan:

– OBDDs

– Boolean encoding

– CTL Symbolic model-checking

Symbolic model checking

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

Plan:

– OBDDs

– Boolean encoding

– CTL Symbolic model-checking – Fairness

– p. 3/65

Symbolic model checking

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

Plan:

– OBDDs

– Boolean encoding

– CTL Symbolic model-checking – Fairness

OBDDs

– p. 4/65

Ordered Binary Decision Trees

[Bryant 1992]

– f : {0, 1}³ → {0, 1}

– Z ⊆ {0, 1}³

– fixed order on variables: x1 < x2 < x3

Ordered Binary Decision Diagrams

OBDD = rooted directed acyclic graph

Attributes of a node v:

– when v is a leaf

– a value val(v) ∈ {0, 1}

– when v is not a leaf

– a variable var(v) ∈ {x1, x2, . . .}

– 2 successor nodes s⁰(v), s¹(v)

The order of variables must be obeyed on every path.

[Bryant 1992]

– p. 6/65

Reduced OBDD

– remove redundant leaves

– remove redundant non-leaves OBDD 7−→ ROBDD

– remove redundant tests

Reduced OBDD = canonical form

Canonical form for a boolean function:

– independent from the initial OBDD

– (strongly) dependent on the order of variables

Naive construction of an OBDD for a boolean formula φ:

φ

 //

 //

Finding an appropriate order of variables is crucial!

– p. 8/65

Order of variables is crucial

a1 ∧ b¹ ∨ a² ∧ b² ∨ a³ ∧ b³

Order of variables is crucial

a1 ∧ b¹ ∨ a² ∧ b² ∨ a³ ∧ b³

a¹ ∧ b¹ ∨ a² ∧ b² ∨ . . . ∨ an ∧ bn

2 · n 2 · (2ⁿ − 1)

– p. 9/65

OBDD size

Heuristic: closely related variables should be close in the order

example of a boolean function lower bound upper bound

symmetric functions O(n) O(n²)

addition (oldest bits) O(n) O(2ⁿ) multiplication (middle bits) O(2ⁿ) O(2ⁿ)

Shannon’s expansion

f = ¬x ∧ f | _x←0 ∨ x ∧ f | _x←1

f|xi←b(x1, . . . , xn) = f (x1, . . . , xi−1, b, xi+1, . . . , xn)

– p. 11/65

Shannon’s expansion

f = ¬x ∧ f | _x←0 ∨ x ∧ f | _x←1

f|xi←b(x1, . . . , xn) = f (x1, . . . , xi−1, b, xi+1, . . . , xn)

v = ¬x ∧ s ⁰ (v) ∨ x ∧ s ¹ (v)

v

~~| |

|

|

B B B B B B

B B

s⁰(v) s¹(v)

OBDDs as an abstract data type

the order of variables the same in all OBDDs

– p. 12/65

OBDDs as an abstract data type

the order of variables the same in all OBDDs

Operations:

f ∨ g, f ∧ g, ¬f , false, true BF 7→ OBDD

f|x←0, f|x←1

OBDDs as an abstract data type

the order of variables the same in all OBDDs

Operations:

f ∨ g, f ∧ g, ¬f , false, true BF 7→ OBDD

f|x←0, f|x←1

∃x. f , ∀x. f QBF 7→ OBDD

– p. 12/65

OBDDs as an abstract data type

the order of variables the same in all OBDDs

Operations:

f ∨ g, f ∧ g, ¬f , false, true BF 7→ OBDD

f|x←0, f|x←1

∃x. f , ∀x. f QBF 7→ OBDD

f = g

OBDDs as an abstract data type

the order of variables the same in all OBDDs

Operations:

f ∨ g, f ∧ g, ¬f , false, true BF 7→ OBDD

f|x←0, f|x←1

∃x. f , ∀x. f QBF 7→ OBDD

f = g

Note: operations on boolean functions, not on values {0, 1}.

– p. 12/65

Implementation of unary operations

– f|x←b

traverse nodes n of OBDD representing f :

– if x > var(n) then recursively traverse s0(n) and s1(n);

– if x < var(n) then stop;

– otherwise replace n by:

s0(n) if b = 0 s1(n) if b = 1

Implementation of unary operations (cont.)

– ∃x. f = f |x←0 ∨ f |x←1 the order of variables remains the same!

Implementation of unary operations (cont.)

– ∃x. f = f |x←0 ∨ f |x←1 the order of variables remains the same!

– ¬f ^?

[Bryant 1992]

Implementation of binary operations

the order of variables the same in all OBDDs

• : {0, 1}² → {0, 1}

for two given OBDDs representing f and g, compute an OBDD representing f • g

f • g = ¬x ∧ (f • g)|x←0 ∨ x ∧ (f • g)|x←1

f • g = ¬x ∧ (f |x←0 • g|x←0) ∨ x ∧ (f |x←1 • g|x←1)

– p. 15/65

Implementation of binary operations

Apply( f, g, • ) f • g (think of f, g as roots of OBDDs ) – f, g leaves: val(f • g) := val(f ) • val(g)

– f leaf, g not: f • g := op(g) – var(f ) = var(g) = x:

var(f • g) := x s⁰(f • g) := s⁰(f ) • s⁰(g) s¹(f • g) := s¹(f ) • s¹(g) – var(f ) = x < y = var(g):

var(f • g) := x s⁰(f • g) := s⁰(f ) • g s¹(f • g) := s¹(f ) • g

f • g = ¬x ∧ (f • g)|x←0 ∨ x ∧ (f • g)|x←1

f • g = ¬x ∧ (f |x←0 • g|x←0) ∨ x ∧ (f |x←1 • g|x←1)

Example: input OBDDs

[Bryant 1992]

(a ∨ b) ∧ c ∨ d a ∧ ¬c ∨ d

– p. 17/65

Example: recursive calls

[Bryant 1992]

Example: result = a ∨ b ∧ c ∨ d

[Bryant 1992]

– p. 19/65

Example: reduced result = a ∨ b ∧ c ∨ d

[Bryant 1992]

Implementation of binary operations

Apply( f, g, • )

– running time: O(|f | · |g|) – result in the canonical form

– p. 21/65

Implementation of binary operations

Apply( f, g, • )

– running time: O(|f | · |g|) – result in the canonical form

Question: f ⇐⇒ g ^?

Implementation of binary operations

Apply( f, g, • )

– running time: O(|f | · |g|) – result in the canonical form

Question: f ⇐⇒ g ^? Question: f = g ^?

– p. 21/65

Variations and extensions

– one OBDD shared by all functions 7→ f = g in constant time

Variations and extensions

– one OBDD shared by all functions 7→ f = g in constant time – edges representing ¬

– p. 22/65

Variations and extensions

– one OBDD shared by all functions 7→ f = g in constant time – edges representing ¬

– OZBDDs (Ordered Zero-supressed BDDs)

Variations and extensions

– one OBDD shared by all functions 7→ f = g in constant time – edges representing ¬

– OZBDDs (Ordered Zero-supressed BDDs) – . . .

– p. 22/65

Boolean encoding

model description

boolean encoding

**

U U U U U U U U U U U U U U U U U U U U U

QBF

implementation

G ##G G G G G G G

model checking = operations on OBDDs OBDD

Model description

– Kripke structure M = (S, S⁰, R, L)

– p. 24/65

Model description

– Kripke structure M = (S, S⁰, R, L)

– S described by m boolean variables: S ≡ {0, 1}^m

Model description

– Kripke structure M = (S, S⁰, R, L)

– S described by m boolean variables: S ≡ {0, 1}^m

– transition relation R : {0, 1}^m × {0, 1}^m → {0, 1}

R(x1, . . . , xm, x^′1, . . . , x^′_m) ∈ {0, 1}

– p. 24/65

Model description

– Kripke structure M = (S, S⁰, R, L)

– S described by m boolean variables: S ≡ {0, 1}^m

– transition relation R : {0, 1}^m × {0, 1}^m → {0, 1}

R(x1, . . . , xm, x^′1, . . . , x^′_m) ∈ {0, 1}

– initial states S0 : {0, 1}^m → {0, 1}

S0(x1, . . . , xm) ∈ {0, 1}

Model description

– Kripke structure M = (S, S⁰, R, L)

– S described by m boolean variables: S ≡ {0, 1}^m

– transition relation R : {0, 1}^m × {0, 1}^m → {0, 1}

R(x1, . . . , xm, x^′1, . . . , x^′_m) ∈ {0, 1}

– initial states S0 : {0, 1}^m → {0, 1}

S0(x1, . . . , xm) ∈ {0, 1}

– atomic properties Lp = {s | p ∈ L(s)} : {0, 1}^m → {0, 1}

Lp(x1, . . . , xm) ∈ {0, 1}

– p. 24/65

Example

ONML HIJK

 // GFED @ABC ?>=< 89:;

''ONML HIJK

gg FED ABC

__

(reachable states)

variables = {x, y}

R = (x ∧ y ∧ x^′ ∧ ¬y^′) ∨ (x ∧ ¬y ∧ x^′ ∧ ¬y^′) ∨ (x ∧ ¬y ∧ x^′ ∧ y^′) S0 = x ∧ y

Lp = y

SMV model – example

MODULE main VAR

request : {Tr, Fa};

state : {ready, busy};

ASSIGN

init(state) := ready;

next(state) := case

state = ready & (request = Tr): busy;

TRUE : {ready,busy};

esac;

SPEC

AG((request = Tr) -> AF state = busy)

– p. 26/65

From a model to OBDD

description of a Kripke structure

_



 //

NO!

From a model to OBDD

description of a Kripke structure

_



 //

NO!

description of a Kripke structure

 //

YES!

– p. 27/65

Compositional model desciption

Synchronous processes:

R = R1 ∧ R² ∧ . . . ∧ Rn

Compositional model desciption

Synchronous processes:

R = R1 ∧ R² ∧ . . . ∧ Rn

Asynchronous processes (interleaving):

R = R^′1 ∨ R^′2 ∨ . . . ∨ R^′_n

R_i^′ = Ri ∧ (V

j6=i Idj)

– p. 28/65

Compositional model desciption

Synchronous processes:

R = R1 ∧ R² ∧ . . . ∧ Rn

Asynchronous processes (interleaving):

R = R^′1 ∨ R^′2 ∨ . . . ∨ R^′_n

R_i^′ = Ri ∧ (V

j6=i Idj) Asynchronous processes (simultaneous execution):

R = R^′1 ∧ R^′2 ∧ . . . ∧ R^′_n

R^′_i = Ri ∨ Idi

Restriction to reachable states

R(xb 1, . . . , xm, x^′1, . . . , x^′_m) = 1 m

R(x1, . . . , xm, x^′1, . . . , x^′_m) ∧ (x1, . . . , xm) reachable

Should we restrict to reachable states?

– p. 29/65

CTL Symbolic model-checking

Reminder

Fixed points in a complete lattice hA, ≤i. Assume A is finite.

Let f : A → A monotonic.

– p. 31/65

Reminder

Fixed points in a complete lattice hA, ≤i. Assume A is finite.

Let f : A → A monotonic.

– the least f.p.: ⊥ ≤ f (⊥) ≤ f²(⊥) ≤ . . . µZ. f(Z)

– the greatest f.p.: ⊤ ≥ f (⊤) ≥ f²(⊤) ≥ . . . νZ. f(Z)

When A finite, the fixed points are reached after ≤ |A| iterations.

Reminder

Fixed points in a complete lattice hA, ≤i. Assume A is finite.

Let f : A → A monotonic.

– the least f.p.: ⊥ ≤ f (⊥) ≤ f²(⊥) ≤ . . . µZ. f(Z)

– the greatest f.p.: ⊤ ≥ f (⊤) ≥ f²(⊤) ≥ . . . νZ. f(Z)

When A finite, the fixed points are reached after ≤ |A| iterations.

Example: hA, ≤i = hP(S), ⊆i EXZ = {s : R(s, s^′) for some s^′ ∈ Z}

– p. 31/65

Reminder

Fixed points in a complete lattice hA, ≤i. Assume A is finite.

Let f : A → A monotonic.

– the least f.p.: ⊥ ≤ f (⊥) ≤ f²(⊥) ≤ . . . µZ. f(Z)

– the greatest f.p.: ⊤ ≥ f (⊤) ≥ f²(⊤) ≥ . . . νZ. f(Z)

When A finite, the fixed points are reached after ≤ |A| iterations.

Example: hA, ≤i = hP(S), ⊆i EXZ = {s : R(s, s^′) for some s^′ ∈ Z}

Z 7→ EX Z µZ. EX Z = ⊥ = ∅ νZ. EX Z = ^?

Reminder

Fixed points in a complete lattice hA, ≤i. Assume A is finite.

Let f : A → A monotonic.

– the least f.p.: ⊥ ≤ f (⊥) ≤ f²(⊥) ≤ . . . µZ. f(Z)

– the greatest f.p.: ⊤ ≥ f (⊤) ≥ f²(⊤) ≥ . . . νZ. f(Z)

When A finite, the fixed points are reached after ≤ |A| iterations.

Example: hA, ≤i = hP(S), ⊆i EXZ = {s : R(s, s^′) for some s^′ ∈ Z}

Z 7→ EX Z µZ. EX Z = ⊥ = ∅ νZ. EX Z = ^?

Z 7→ p ∨ EX Z µZ. p ∨ EX Z = ^?

– p. 31/65

Example

EFp = µZ. p ∨ EX Z Z 7→ p ∨ EX Z

false

7654 0123 //?>=< 89:;

// 7654 0123 //

__ 7654 0123

p ∨ EX false ≡ p

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

// 7654 0123 //

__ 7654 0123

p ∨ EX p

7654 0123 '&%$ !"# //?>=< 89:; /.-, ()*+

// 7654 0123 //

__ 7654 0123

p ∨ EX (p ∨ EX p)

7654 0123 '&%$ !"# //?>=< 89:; /.-, ()*+

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

__ 7654 0123

CTL via fixed points

– EFφ = µZ. φ ∨ EX Z Z 7→ φ ∨ EX Z

– AFφ = µZ. φ ∨ AX Z Z 7→ φ ∨ AX Z

– EGφ = νZ. φ ∧ EX Z Z 7→ φ ∧ EX Z

– AGφ = νZ. φ ∧ AX Z Z 7→ φ ∧ AX Z

– Eφ U ψ = µZ. ψ ∨ (φ ∧ EX Z) Z 7→ ψ ∨ (φ ∧ EX Z) – Aφ U ψ = µZ. ψ ∨ (φ ∧ AX Z) Z 7→ ψ ∨ (φ ∧ AX Z) – . . .

– p. 33/65

Example

EGp = νZ. p ∧ EX Z Z 7→ p ∧ EX Z

true

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

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

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

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

p ∧ EX true ≡ p

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

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

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

// 7654 0123FED XX ABC

p ∧ EX p

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

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

//?>=< 89:;

// 7654 0123FED XX ABC

p ∧ EX (p ∧ EX p)

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

//?>=< 89:;

//?>=< 89:;

// 7654 0123FED XX ABC

CTL Symbolic model checking

CTL (¬, ∧, ^EX, ^{E _ U _} , ^{EG )} (these connectives are sufficient)

OBDD : CTL 7→ OBDD

OBDD(φ) represents {s | s  φ}

– p. 35/65

CTL Symbolic model checking

CTL (¬, ∧, ^EX, ^{E _ U _} , ^{EG )} (these connectives are sufficient)

OBDD : CTL 7→ OBDD

OBDD(φ) represents {s | s  φ}

– OBDD(p) := OBDD representing Lp

CTL Symbolic model checking

CTL (¬, ∧, ^EX, ^{E _ U _} , ^{EG )} (these connectives are sufficient)

OBDD : CTL 7→ OBDD

OBDD(φ) represents {s | s  φ}

– OBDD(p) := OBDD representing Lp

– OBDD(¬φ) := ¬OBDD(φ)

– p. 35/65

CTL Symbolic model checking

CTL (¬, ∧, ^EX, ^{E _ U _} , ^{EG )} (these connectives are sufficient)

OBDD : CTL 7→ OBDD

OBDD(φ) represents {s | s  φ}

– OBDD(p) := OBDD representing Lp

– OBDD(¬φ) := ¬OBDD(φ)

– OBDD(φ ∧ ψ) := OBDD(φ) ∧ OBDD(ψ)

Symbolic model checking ( EX _ )

OBDD : CTL → OBDD OBDD(φ) represents {s | s  φ}

OBDD( EX φ) := ∃~x^′. R(~x, ~x^′) ∧ f [~x^′/~x] where f = OBDD(φ) OBDD( EX φ) := EXf = EXOBDD(φ)

EXφ EXZ EXf

– p. 36/65

Order of variables

∃~x^′. R(~x, ~x^′) ∧ f [~x^′/~x])

~x = x¹, x², . . . , xm

x1 < x2 < . . . < xm

x¹ < x^′1 < x² < x^′2 < . . . < xm < x^′_m xi < xj if and only if x^′_i < x^′_j

Symbolic model checking ( E _ U _ )

OBDD : CTL → OBDD OBDD(φ) represents {s | s  φ}

OBDD( E φ U ψ) := µZ. g ∨ (f ∧ EXZ) where f = OBDD(φ) g = OBDD(ψ) h 7→ g ∨ (f ∧EXh)

h 7→ g ∨ (f ∧∃~x^′. R(~x, ~x^′) ∧ h[~x^′/~x])

– p. 38/65

Symbolic model checking ( E _ U _ )

OBDD : CTL → OBDD OBDD(φ) represents {s | s  φ}

OBDD( E φ U ψ) := µZ. g ∨ (f ∧ EXZ) where f = OBDD(φ) g = OBDD(ψ) h 7→ g ∨ (f ∧EXh)

h 7→ g ∨ (f ∧∃~x^′. R(~x, ~x^′) ∧ h[~x^′/~x])

Implement computation of the approximations of lfp by OBDDs:

h0 ≡ false

h1 ≡ g ∨ (f ∧ EXh0) ≡ g

h² ≡ g ∨ (f ∧ EXh¹) ≡ g ∨ (f ∧ EXg)

h³ ≡ . . . ≡ g ∨ (f ∧ EX(g ∨ (f ∧ EXg)))

Symbolic model checking ( EG _ )

OBDD : CTL → OBDD OBDD(φ) represents {s | s  φ}

OBDD( EG φ) := νZ. f ∧ EXZ where f = OBDD(φ)

h 7→ f ∧ EXh

h 7→ f ∧ ∃~x^′. R(~x, ~x^′) ∧ h[~x^′/~x]

– p. 39/65

Symbolic model checking ( EG _ )

OBDD : CTL → OBDD OBDD(φ) represents {s | s  φ}

OBDD( EG φ) := νZ. f ∧ EXZ where f = OBDD(φ)

h 7→ f ∧ EXh

h 7→ f ∧ ∃~x^′. R(~x, ~x^′) ∧ h[~x^′/~x]

Implement computation of the approximations of gfp by OBDDs, as bofore.

EXφ EφUψ EGφ

EXZ EZ UZ^′ EGZ

EXf Ef Ug EGf

– p. 40/65

Graph diameter

Efficiency of SMC depends on the diameter of M .

Fairness

– p. 42/65

Fair CTL

F = {ψ¹, . . . , ψn}, ψi ∈ CTL 7→ F = {Z¹, . . . , Zn}

s F p ⇐⇒ p ∈ L(s) ∧ ∃ fair Π from s s F Aφ U ψ ⇐⇒ ∀ fair Π from s . Π  φ U ψ s F Eφ U ψ ⇐⇒ ∃ fair Π from s . Π  φ U ψ s F AXφ ⇐⇒ ∀ fair Π from s . Π  X φ s F EXφ ⇐⇒ ∃ fair Π from s . Π  X φ

F = {h¹, . . . , hn}, hi ∈ OBDD

Fair EG

F = {ψ¹, . . . , ψn}, ψi ∈ CTL 7→ F = {Z¹, . . . , Zn}

EGφ = {s | s F EGφ} = the greatest Z s.t. if s ∈ Z then – s  φ

– ∀i ≤ n . ∃s^′ . s −→ . . . −→ s^′ ∈ Zi ∩ Z, s^′ 6= s, all intermediate states satisfy φ

– p. 44/65

Fair EG

F = {ψ¹, . . . , ψn}, ψi ∈ CTL 7→ F = {Z¹, . . . , Zn}

EGφ = {s | s F EGφ} = the greatest Z s.t. if s ∈ Z then – s  φ

– ∀i ≤ n . ∃s^′ . s −→ . . . −→ s^′ ∈ Zi ∩ Z, s^′ 6= s, all intermediate states satisfy φ

EGφ = νZ. φ ∧ Vn

i=1 EX Eφ U (ψi ∧ Z)

Fair EG

F = {ψ¹, . . . , ψn}, ψi ∈ CTL 7→ F = {Z¹, . . . , Zn}

EGφ = {s | s F EGφ} = the greatest Z s.t. if s ∈ Z then – s  φ

– ∀i ≤ n . ∃s^′ . s −→ . . . −→ s^′ ∈ Zi ∩ Z, s^′ 6= s, all intermediate states satisfy φ

EGφ = νZ. φ ∧ Vn

i=1 EX Eφ U (ψi ∧ Z) EGφ = νZ. φ ∧ Vn

i=1 EXµY.(ψi ∧ Z) ∨ (φ ∧ EX Y ) alternation!

– p. 44/65

Fair EG

Thm:

EGφ = νZ. φ ∧

^n i=1

EX Eφ U (ψi ∧ Z)

Proof:

EGφ = φ ∧

^n i=1

EX Eφ U (ψi ∧ EGφ)

Z = φ ∧

^n i=1

EX Eφ U (ψi ∧ Z) =⇒ Z ⊆ EGφ

Fair symbolic model checking ( EG _ )

OBDD : CTL → OBDD OBDD(φ) represents {s | s F φ}

F = {ψ¹, . . . , ψn}, ψi ∈ CTL 7→ F = {h1, . . . , hn}, hi ∈ OBDD

OBDD( EG φ) := νZ. f ∧ Vn

i=1 EX Ef U (hi ∧ Z)

where f = OBDD(φ)

Z 7→ f ∧

^n i=1

EX Ef U (hi ∧ Z)

– p. 46/65

Fair CTL symbolic model checking

fair := OBDD( EG true)

OBDD( EX φ) := ∃~x^′. R(~x, ~x^′) ∧ f (~x^′) ∧ fair(~x^′)

where f = OBDD(φ)

OBDD( E φ U ψ) := µZ. (g ∧ fair) ∨ (f ∧ EXZ)

where f = OBDD(φ) g = OBDD(ψ)

How to compute EX f ?

– p. 48/65

EX f by AndExist

EXf := ∃~x^′. R(~x, ~x^′) ∧ f (~x^′)

operation ∃∧(g, h, V ) := ∃V. g ∧ h (V – set of variables)

R(x¹, . . . , xm, x^′1, . . . , x^′_m)

f (x1, . . . , xm) 7→ f^′(x^′1, . . . , x^′_m) xi ≤ xj ⇐⇒ x^′i ≤ x^′j

EXf = ∃∧(R, f^′,{x^′1, . . . , x^′_m})

AndExist

∃∧( f, g, V ) ( ∃V. f ∧ g )

– f, g leaves: val(∃∧(f, g, V )) := val(f ) ∧ val(g) – f a leaf, g not: ∃∧(f, g, V ) := false or ∃V. g – x = var(f ) = var(g):

l := ∃∧(s⁰(f ), s⁰(g), V ), h := ∃∧(s¹(f ), s¹(g), V ) – x ∈ V : ∃∧(f, g, V ) := l ∨ h

– x /∈ V : s⁰(∃∧(f, g, V )) := l s¹(∃∧(f, g, V )) := h – x = var(f ) < var(g): . . .

f • g = ¬x ∧ (f |x←0 • g|x←0) ∨ x ∧ (f |x←1 • g|x←1)

– p. 50/65

R is not monolytic

EXf := ∃~x^′. R(~x, ~x^′) ∧ f (~x^′)

Asynchronous model: R = R^′1 ∨ R^′2 ∨ . . . ∨ R^′_n

R^′_i = Ri ∧ V

j6=i Idj

Synchronous model: R = R1 ∧ R2 ∧ . . . ∧ Rn

Can one profit from this additional structure ?

Asynchronous model: R = R^′1 ∨ R^′2 ∨ . . . ∨ R^′_n

R^′_i = Ri ∧ V

j6=i xj = x^′_j

∃~x^′. R ∧ f (~x^′) ≡ ∃~x^′. (R^′1 ∧ f (~x^′)) ∨ . . . ∨ (R^′_n ∧ f (~x^′))

≡ ∃~x^′. R^′1 ∧ f (~x^′)

∨ . . . ∨ ∃~x^′. R^′_n ∧ f (~x^′)

∃~x^′. R^′_i ∧ f (~x^′) ≡ ∃~x^′. Ri ∧ (V

j6=i xj = x^′_j) ∧ f (~x^′)

≡ ∃x^′_i. Ri(~x, x^′_i) ∧ f (x1, . . . , xi−1, x^′_i, xi+1, . . . , xm)

– p. 52/65

Synchronous model: R = R1 ∧ R² ∧ . . . ∧ Rn

∃~x^′. R¹(~x, ~x^′) ∧ . . . ∧ Rn(~x, ~x^′) ∧ f (~x^′)

– relations Ri are local – „early” quantification – heuristics

Example: 3-bit counter

R⁰(~x, x^′0) = (x^′0 = ¬x⁰)

R1(~x, x^′1) = (x^′1 = x0 xor x1)

R2(~x, x^′2) = (x^′2 = (x0 ∧ x1) xor x2)

∃x^′2∃x^′1∃x^′0. f (x^′0, x^′1, x^′2) ∧ R⁰(~x, x^′0) ∧ R¹(~x, x^′1) ∧ R²(~x, x^′2)

∃x^′2 ∃x^′1∃x^′0. f (x^′0, x^′1, x^′2) ∧ R⁰(~x, x^′0) ∧ R¹(~x, x^′1)

∧ R²(~x, x^′2)

∃x^′2 ∃x^′1 ∃x^′0. f (x^′0, x^′1, x^′2) ∧ R⁰(~x, x^′0)

∧ R¹(~x, x^′1)

∧ R²(~x, x^′2)

∃x^′2 ∃x^′1 ∃x^′0. f (x^′0, x^′1, x^′2) ∧ R⁰(x⁰, x^′0)

∧ R¹(x⁰, x¹, x^′1)

∧ R²(x⁰, x¹, x², x^′2)

– p. 54/65

Example: 3-bit counter

∃x^′2 ∃x^′1 ∃x^′0 f (x^′0, x^′1, x^′2) ∧ R⁰(x⁰, x^′0)

∧ R1(x0, x1, x^′1)

∧ R2(x0, x1, x2, x^′2)

– sequence of ∃∧ operations

– optimal order of processes (not variables this time):

– early elimination of variables (∃) – late introducing of variables

(Counter)examples

– p. 56/65

Counterexample

counterexample for AFφ = example for EG¬φ

Counterexample

counterexample for AFφ = example for EG¬φ counterexample for AGφ = example for EF¬φ ( fair counterexample is always an infinite path )

Counterexample

counterexample for AFφ = example for EG¬φ counterexample for AGφ = example for EF¬φ ( fair counterexample is always an infinite path )

counterexample for EFφ = ^? counterexample for EGφ = ^?

Symbolic counterexample

How to compute an example for:

– EGφ – Eφ U ψ – EXφ

symbolically ?

– p. 58/65

Example for E _ U _

Computation of Ef U g:

Q0 ⊆ Q¹ ⊆ . . . (1 ≤ i ≤ n)

s ∈ Qj ⇐⇒ g may be reached from s "via f " by ≤ j transitions

Computing an example for s  E f U g:

– let j minimal s.t. s ∈ Qj

– reconstruct s = sj −→ sj−1 −→ . . . −→ s0 ∈ g

Symbolic counterexample

How to compute a fair example for:

– EGφ – Eφ U ψ – EXφ

symbolically ?

[Clarke, Grumberg, Long 1994]

– p. 60/65

Fair example for EG _

EGf = νZ. f ∧

^n i=1

EX Ef U (hi ∧ Z)

last iteration Z 7→ f ∧ Vn

i=1 EX Ef U (hi ∧ Z):

computation of Ef U (hi ∧ Z): Z = EGf Qⁱ0 ⊆ Qⁱ1 ⊆ . . . (1 ≤ i ≤ n)

Fair example for EG _

EGf = νZ. f ∧

^n i=1

EX Ef U (hi ∧ Z)

s := s⁰ initial state I := {1, . . . , n}

repeat

find t s.t. s −→ t, t ∈ Qⁱ_j, i ∈ I, j minimal

reconstruct t = tj −→ tj−1 −→ . . . −→ t0 ∈ (hi ∧ EGf) I := I \ {i | t⁰ ∈ hi}

s := t0 I := I \ {i | t ∈ Qⁱj}

until I = ∅

s^′ := s 7→ path s⁰ −→ . . . −→ s^′

– p. 61/65

Fair example for EG _

[Clarke, Grumberg, Long 1994]

Fair example for EG _

EGf = νZ. f ∧

^n i=1

EX Ef U (hi ∧ Z)

we have a path s0 −→ . . . −→ s^′ let t = the first t0

(a) if s^′  EX E f U {t} stop

otherwise restart: s⁰ := s^′, I := {1, . . . , n}

improvement:

(b) compute Ef U{t}

as long as ¬(s  E f U {t}), restart: s⁰ := s, I := {1, . . . , n}

– p. 63/65

Fair example for E _ U _, EX _

Example for Eφ U (ψ ∧ fair) or EX (φ ∧ fair) extend with a fair example for EG true.

What else can be computed using OBDDs ?

– Lω(A) 6= ∅ fair EG true

– LTL model checking

– Lω(A1) ⊆ Lω(A2) A1 × A2  A ( G F q¹ =⇒ G F q2) – µ-calculus model checking

– reachable states – deadlocks

– (bi)simulation equivalence – . . .

– p. 65/65

What else can be computed using OBDDs ?

– Lω(A) 6= ∅ fair EG true

– LTL model checking

– Lω(A1) ⊆ Lω(A2) A1 × A2  A ( G F q¹ =⇒ G F q2) – µ-calculus model checking

– reachable states – deadlocks

– (bi)simulation equivalence – . . .

OBDDs are routinely used in hardware

industry nowadays