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

4.1 Time Reversal Step

Time Reversal Step [Slide 18]

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

Let F^{r} denotes the time reversed version of fusion logic formula
F.

Let reverse(σ) denote the time reversed interval of σ:

reverse(σ_{0}…σ_{|σ|})≜σ_{|σ|}…σ_{0}

M⟦F^{r}⟧(σ) = tt iﬀ M⟦F⟧(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}

=

⟨E^{r}⟩L^{r}

(ﬁn(p))^{r}

=

p

true^{r}

=

true

(¬L)^{r}

=

¬(L^{r})

(L_{1}∨L_{2})^{r}

=

L_{1}^{r}∨L_{2}^{r}

fusion expressions

transitions

(test(W))^{r}

=

test(W)

(step(T))^{r}

=

step(T^{r})

(E_{1}∨E_{2})^{r}

=

E_{1}^{r}∨E_{2}^{r}

(E_{1};E_{2})^{r}

=

E_{2}^{r};E_{1}^{r}

(E^{∗})^{r}

=

(E^{r})^{∗}

(W)^{r}

=

W

W^{r}

=

W

(T_{1}∨T_{2})^{r}

=

T_{1}^{r}∨T_{2}^{r}

(¬T)^{r}

=

¬(T^{r})

Time Reversal Step [Slide 20]

The following holds

Let L be a left fusion logic formula then L^{r} is a right fusion logic
formula.

Let L be a left fusion logic formula then M⟦L⟧(σ) =
tt
iﬀ
M⟦L^{r}⟧(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=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)

Reduction Step [Slide 22]

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})

whereX_{1}isX∨⟨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.

Reduction Step [Slide 23]

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 Step [Slide 24]

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^{∗}

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= 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))

4.3 BDD Step

BDD Step [Slide 27]

Transforminit∧_{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

BDD Step [Slide 28]

We know that invariantI 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

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= r_{X1}∨r_{X3} and corresponding invariant:

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 ∨_{0≤i≤n}Δ_{i}
representing the set of all states so far reachable from Γ_{1}. If
(∨_{0≤i≤n}Δ_{i}) ≡ (∨_{0≤i≤n+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 r_{i} 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 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.