4 Decision Procedure for Fusion Logic

  4.1 Time Reversal Step
  4.2 Reduction Step
  4.3 BDD Step

Decision Procedure [Slide 17]

4.1 Time Reversal Step

Time Reversal Step [Slide 18]

Transform a left fusion formula into a right fusion logic formula.

Time Reversal Step [Slide 19]

Rules to rewrite left fusion logic formulae into right fusion logic formulae

left fusion formulae
((LE)r
=
ErLr
(fin(p))r
=
p
truer
=
true
(¬L)r
=
¬(Lr)
(L1 L2)r
=
L1r L2r
fusion expressions
transitions
(test(W))r
=
test(W)
(step(T))r
=
step(Tr)
(E1 E2)r
=
E1r E2r
(E1 ; E2)r
=
E2r ; E1r
(E)r
=
(Er)
( W)r
=
W
Wr
=
W
(T1 T2)r
=
T1r T2r
(¬T)r
=
¬(Tr)

Time Reversal Step [Slide 20]

The following holds

4.2 Reduction Step

Reduction Step [Slide 21]

Transform right fusion logic formula R into an equivalent reduced form init rI where

Reduction Step [Slide 22]

Let X,X1 and X2 denote non state formulae and w a state formula then the definition of Transition formula k(f) is as follows:

For k ∈{0,1}

R
k(R)
W
true
test(W)X
k(X)
step(T)X
k = 0 : (rstep(T)X (T ℛ′0(X))) ∧ℛ0(X)
k = 1 : 0(X)
E1 E2X
k(E1X ∨⟨E2X)
E1 ; E2X
k(E1⟩⟨E2X)
EX
(rEX ≡ℛ′1(X1)) ∧ℛ1(X1)
where X1 is X ∨⟨c(E)rEX
¬X
k(X)
X1 X2
k(X1) ∧ℛ0(X2)

So only the step(t) and e case will introduce a dependent variable.

Reduction Step [Slide 23]

Let X,X1 and X2 denote non state formulae and w a state formula then the definition of state formula ℛ′k(f) is as follows:

For k ∈{0,1}

R
ℛ′k(R)
W
W
test(W)X
W ∧ℛ′k(X)
step(T)X
k = 0 : rstep(T)X
k = 1 : T ℛ′0(X)
E1 E2X
ℛ′k(E1X ∨⟨E2X)
E1 ; E2X
ℛ′k(E1⟩⟨E2X)
EX
rEX
¬X
¬ℛ′k(X)
X1 X2
ℛ′k(X1) ∨ℛ′k(X2)

Reduction Step [Slide 24]

Reduction function for EX is a bit more involved because e could be valid for intervals with only one state. Solution: a function c is introduced which transforms an arbitrary fusion expression e into another formula c(e) such that c(e) E moree holds. Note: EW ≡⟨c(E)W holds.

E
c(E)
test(W)
test(¬true)
step(T)
step(T)
E1 E2
c(E 1) c(E2)
E1 ; E2
c(E1) ; E2 E1 ; c(E2)
E
c(E) ; E

Reduction Step [Slide 25]

The following holds

Example [Slide 26]

Given a right fusion logic formula

step(A)(B C) ∨⟨step(A) ; test(B)D

The Reduction Step yields:

init = rX1 rX3 where X1 step(A)(B C) and X3 step(A)⟩⟨test(B)D.

The corresponding invariant I is

I = (rX1 (B C) (A rX1)) (rX3 A (B D))

4.3 BDD Step

BDD Step [Slide 27]

Transform init rI into BDD based satisfiability problem.

init: a state formula
I: an invariant, i=1i=k(rXi ti) (for k 1) where
rXi is a dependent variable and
ti is a transition formula

Let us examine the ‘Always’ operator

init rI
I
I
I
— —
I
— —
— —
I
— —
— —
— —
init

BDD Step [Slide 28]

We know that invariant I only contains (next) as temporal operator. So it can only constrain the first two states of each suffix interval.

init rI
I
I
I
I
I
init

BDD Step [Slide 29]

Introducing BDDs Γi’s:

init I
Γ3
Γ2
Γ2
Γ 2
Γ2
Γ1

Example [Slide 30]

Given right fusion logic formula

step(A)(B C) ∨⟨step(A) ; test(B)D

With Init = rX1 rX3 and corresponding invariant:

I = (rX1 (B C) (A rX1)) (rX3 A (B D))

Then Γ1 = rX1 rX3 and

Γ2 = (rX1 (B C) (A rX1)) (rX3 A (B′∧ D))

and

Γ3 = (rX1 (B C) (A false)) (rX3 A false)

BDD Step [Slide 31]

Encoding as a BDD-based satisfiability problem:

BDD Step [Slide 32]

To construct a satisfying interval (in case F is satisfiable) we proceed as follows.

Let Δm be that set of states for which Γ3 Δm is true.

Implementation [Slide 33]

Implementation of decision procedure

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023