ITL
© 1996-2018







4 Decision Procedure for Fusion Logic

Decision Procedure [Slide 17]

  • Time Reversal Step:

    transform a left fusion logic formula into a right fusion logic formula

  • Reduction Step:

    transform right fusion logic formula R into init rI

  • BDD Step:

    transform init rI into a BDD-based satisfiability problem

4.1 Time Reversal Step

Time Reversal Step [Slide 18]

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

  • Let Fr denotes the time reversed version of fusion logic formula F.
  • Let reverse(σ) denote the time reversed interval of σ:

    reverse(σ0σ|σ|) σ|σ|σ0

  • MFr(σ) = tt iff MF(reverse(σ)) = tt

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

  • Let L be a left fusion logic formula then Lr is a right fusion logic formula.
  • Let L be a left fusion logic formula then ML(σ) = tt iff MLr(reverse(σ)) = tt

4.2 Reduction Step

Reduction Step [Slide 21]

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

  • init: a state formula

    init ℛ′0(f)

  • I: an invariant, i=1i=k(rXi ti) (for k 1) where
    rXi is a dependent Boolean variable (not appearing in F)
    ti is a transition formula

    I 0(f)

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(E1E2X)
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(E1E2X)
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

  • Let R be a right fusion Logic formula and dep(R) be the dependent variables introduced by ℛ′k(R) and k(R) (k = 0, 1) then

    R dep(R) (ℛ′k(R) k(R))

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:

  • Γ1 represents the state formula init.
  • Γ2 captures all pairs of states corresponding to two state intervals satisfying invariant I. This can be done by replacing all variables in the scope of any by a primed version and delete the .
  • Γ3 captures the behaviour of invariant I in an interval with only 1 state. This can be done by replacing each construct by false, i.e., ¬true.

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:

  • We use Γ2 and Γ1 to iteratively calculate a sequence of BDDs Δ0,, Δn, so that for any n, Δn described all states which can be reached from Γ1 in exactly n steps using Γ2.
  • We determine at each iteration whether BDD Γ3 Δn is true or not. If false we must continue to iterate and if true then there is exists some state satisfying Γ3 which can be reached in n steps from Γ1, so we can stop the iteration, i.e., original f is satisfiable.
  • During the iteration process we maintain a BDD 0inΔi representing the set of all states so far reachable from Γ1. If ( 0inΔi) ( 0in+1Δi), i.e., no new states are found, then we stop the iteration and if we can’t find a state that satisfies Γ3 then original f is not satisfiable.

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.

  • If there are no independent variables (only ri variables) then any interval of length m will satisfy F.
  • If there are independent variables then Find a value assignment σm for the independent variables for BDD Δm, i.e., choose one state σm of Δm.

    Compute Prm1 denoting those states of Δm1 that lead via Γ2 to state σm (weakest precondition of Γ2 and σm). Again choose one state σm1 of Prm1.

    Continue until we reach Pr0 and then choose state σ0.

    The states σ0σm1σm will then represent a (minimal) satisfying interval σ for F.

Implementation [Slide 33]

Implementation of decision procedure







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL