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
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 ∧rI 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)
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 : (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.
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 : 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 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 ∧moree holds. Note: ⟨E∗⟩W ≡⟨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∗ |
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 = 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))
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 |
|||||
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 |
|||||
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 = 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 ∧ r′X1)) ∧ (rX3 ≡ A ∧ (B′∧ D′))
and
Γ3 = (rX1 ≡ (B ∨ C) ∨ (A ∧false)) ∧ (rX3 ≡ A ∧false)
Encoding as a BDD-based satisfiability problem:
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 independent variables then Find a value assignment σm for the independent variables for BDD Δm, i.e., choose one state σm of Δm.
Compute Prm−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 Prm−1.
Continue until we reach Pr0 and then choose state σ0.
The states σ0…σm−1σm will then represent a (minimal) satisfying interval σ for F.
Implementation of decision procedure