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 ∧_{r}I
BDD Step:
transform init ∧ _{r}I into a BDDbased satisﬁability problem
Transform a left fusion formula into a right fusion logic formula.
Let reverse(σ) denote the time reversed interval of σ:
reverse(σ_{0}…σ_{σ}) ≜ σ_{σ}…σ_{0}
Rules to rewrite left fusion logic formulae into right fusion logic formulae
left fusion formulae 



fusion expressions  transitions 




The following holds
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=1}^{i=k}(r_{Xi} ≡ t_{i}) (for k ≥ 1) where
r_{Xi} is a dependent Boolean variable (not appearing in F) 
t_{i} is a transition formula 
I ≜ℛ_{0}(f)
Let X,X_{1} and X_{2} 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) 

⟨E_{1} ∨E_{2}⟩X  ℛ_{k}(⟨E_{1}⟩X ∨⟨E_{2}⟩X) 
⟨E_{1} ; E_{2}⟩X  ℛ_{
k}(⟨E_{1}⟩⟨E_{2}⟩X) 
⟨E^{∗}⟩X 
(r_{⟨E∗⟩X} ≡ℛ′_{1}(X_{1})) ∧ℛ_{1}(X_{1}) 
where X_{1} is X ∨⟨c(E)⟩r_{⟨E∗⟩X} 

¬X 
ℛ_{k}(X) 
X_{1} ∨X_{2} 
ℛ_{k}(X_{1}) ∧ℛ_{0}(X_{2}) 
So only the step(t) and e^{∗} case will introduce a dependent variable.
Let X,X_{1} and X_{2} 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) 

⟨E_{1} ∨E_{2}⟩X  ℛ′_{k}(⟨E_{1}⟩X ∨⟨E_{2}⟩X) 
⟨E_{1} ; E_{2}⟩X 
ℛ′_{k}(⟨E_{1}⟩⟨E_{2}⟩X) 
⟨E^{∗}⟩X 
r_{⟨E∗⟩X} 
¬X 
¬ℛ′_{k}(X) 
X_{1} ∨X_{2} 
ℛ′_{k}(X_{1}) ∨ℛ′_{k}(X_{2}) 
Reduction function for ⟨E^{∗}⟩X 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 ∧more_{e} holds. Note: ⟨E^{∗}⟩W ≡⟨c(E)^{∗}⟩W holds.
E 
c(E) 
test(W) 
test(¬true) 
step(T)  step(T) 
E_{1} ∨ E_{2}  c(E_{
1}) ∨ c(E_{2}) 
E_{1} ; E_{2} 
c(E_{1}) ; E_{2} ∨ E_{1} ; c(E_{2}) 
E^{∗} 
c(E) ; E^{∗} 
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))
Given a right fusion logic formula
⟨step(A)^{∗}⟩(B ∨ C) ∨⟨step(A) ; test(B)⟩D
The Reduction Step yields:
init = r_{X1} ∨ r_{X3} where X_{1} ≜⟨step(A)^{∗}⟩(B ∨ C) and X_{3} ≜⟨step(A)⟩⟨test(B)⟩D.
The corresponding invariant I is
I = (r_{X1} ≡ (B ∨ C) ∨ (A ∧ r_{X1})) ∧ (r_{X3} ≡ A ∧(B ∧ D))
Transform init ∧_{r}I into BDD based satisﬁability problem.
init: a state formula 
I: an invariant, ∧ _{i=1}^{i=k}(r_{Xi} ≡ t_{i}) (for k ≥ 1) where 
r_{Xi} is a dependent variable and 
t_{i} is a transition formula 
Let us examine the ‘Always’ operator
init ∧_{r}I 
● 
● 
● 
● 
● 
⟨I⟩ 

⟨—I—⟩ 

⟨—I—  — —⟩  
⟨—I— 
— — 
— —⟩ 

⟨—I— 
— — 
— — 
— —⟩ 

init 

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 ∧_{r}I 
● 
● 
● 
● 
● 
⟨I⟩ 

⟨—I—⟩ 

⟨—I—⟩  
⟨—I—⟩ 

⟨—I—⟩ 

init 

Introducing BDDs Γ_{i}’s:
init ∧ I 
● 
● 
● 
● 
● 
Γ_{3} 

⟨—Γ_{2}—⟩ 

⟨—Γ_{2}—⟩  
⟨—Γ_{
2}—⟩  
⟨—Γ_{2}—⟩ 

Γ_{1} 

Given right fusion logic formula
⟨step(A)^{∗}⟩(B ∨ C) ∨⟨step(A) ; test(B)⟩D
With Init = r_{X1} ∨ r_{X3} and corresponding invariant:
I = (r_{X1} ≡ (B ∨ C) ∨ (A ∧ r_{X1})) ∧ (r_{X3} ≡ A ∧(B ∧ D))
Then Γ_{1} = r_{X1} ∨ r_{X3} and
Γ_{2} = (r_{X1} ≡ (B ∨ C) ∨ (A ∧ r′_{X1})) ∧ (r_{X3} ≡ A ∧ (B′∧ D′))
and
Γ_{3} = (r_{X1} ≡ (B ∨ C) ∨ (A ∧false)) ∧ (r_{X3} ≡ A ∧false)
Encoding as a BDDbased satisﬁability problem:
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 independent variables then Find a value assignment σ_{m} for the independent variables for BDD Δ_{m}, i.e., choose one state σ_{m} of Δ_{m}.
Compute Pr_{m−1} denoting those states of Δ_{m−1} that lead via Γ_{2} to state σ_{m} (weakest precondition of Γ_{2} and σ_{m}). Again choose one state σ_{m−1} of Pr_{m−1}.
Continue until we reach Pr_{0} and then choose state σ_{0}.
The states σ_{0}…σ_{m−1}σ_{m} will then represent a (minimal) satisfying interval σ for F.
Implementation of decision procedure