### 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 satisﬁability problem

#### 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 iﬀ MF(reverse(σ)) = tt

#### Time Reversal Step [Slide 19]

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

left fusion formulae
 ((L⟨E⟩)r = ⟨Er⟩Lr (ﬁn(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 iﬀ MLr(reverse(σ)) = tt

#### 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 deﬁnition 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 : (r⟨step(T)⟩X ≡ (T ∧ℛ′0(X))) ∧ℛ0(X) k = 1 : ℛ0(X) ⟨E1 ∨ E2⟩X ℛk(⟨E1⟩X ∨⟨E2⟩X) ⟨E1 ; E2⟩X ℛk(⟨E1⟩⟨E2⟩X) ⟨E∗⟩X (r⟨E∗⟩X ≡ℛ′1(X1)) ∧ℛ1(X1) where X1 is X ∨⟨c(E)⟩r⟨E∗⟩X ¬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 deﬁnition 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 : r⟨step(T)⟩X k = 1 : T ∧ℛ′0(X) ⟨E1 ∨ E2⟩X ℛ′k(⟨E1⟩X ∨⟨E2⟩X) ⟨E1 ; E2⟩X ℛ′k(⟨E1⟩⟨E2⟩X) ⟨E∗⟩X r⟨E∗⟩X ¬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))

#### BDD Step [Slide 27]

Transform init rI into BDD based satisﬁability 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 ﬁrst two states of each suﬃx 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 satisﬁability 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 satisﬁable.
• 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 ﬁnd a state that satisﬁes Γ3 then original f is not satisﬁable.

#### BDD Step [Slide 32]

To construct a satisfying interval (in case F is satisﬁable) 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-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL