Decision Procedure for Fusion Logic

4 Decision Procedure for Fusion Logic

4.1 Reduction Step
4.2 BDD Step

Decision Procedure [Slide 20]

The decision procedure is discussed in details in [5].

Reduction Step:

transform fusion logic formula FL into ∃X init ∧ I where X is a set of propositional dependency variables not occurring in FL and I is future transition formula
BDD Step:

transform init ∧ I into a BDD-based satisﬁability problem

4.1 Reduction Step

Reduction Step [Slide 21]

Transform a fusion logic formula FL into an equivalent reduced form init ∧ I

1.

Transform FL into ﬁnit ∧ T where

ﬁnit: initial state,

ﬁnit ≜ℛ′₀(FL)
T: transition relation, of the form

∧ _i=1^k(r_{X_i} ≡ FT_i) ∧ ∧ _j=1ⁿ(r_{Y _j} ≡ PT_j) where, r_{X_i} and r_{Y _j} are dependent Boolean variables (not appearing in FL) and FT_i is a future transition formula and PT_j is a past transition formula:

T ≜ℛ₀(FL)

2.

Transform ﬁnit ∧ T into init ∧ I

where

init is a state formula
I is a future transition formula

Reduction Step [Slide 22]

Let X,X₁ and X₂ denote non state formulae and w a state formula then the deﬁnition of future Transition formula ℛ_k(FL) is as follows:

For k ∈{0,1}

FL	ℛ_k(FL)

W	true
⟨test(W)⟩X	ℛ_k(X)
⟨step(FT)⟩X	k = 0 : (r_{⟨step(FT)⟩X} ≡(FT ∧ℛ′₀(X))) ∧ℛ₀(X)
	k = 1 : ℛ₀(X)
⟨FE₁ ∨FE₂⟩X	ℛ_k(⟨FE₁⟩X ∨⟨FE₂⟩X)
⟨FE₁ ; FE₂⟩X	ℛ_k(⟨FE₁⟩⟨FE₂⟩X)
⟨FE^∗⟩X	(r_{⟨FE^∗⟩X} ≡ℛ′₁(X₁)) ∧ℛ₁(X₁)
	where X₁ is X ∨⟨c(FE)⟩r_{⟨FE^∗⟩X}
X₁ U X₂	(r_X₁UX₂ ≡(ℛ′₁(X₂) ∨(ℛ′₁(X₁) ∧r_X₁UX₂))
X	ℛ_k(⟨step(true)⟩X)

So only the step(FT), FE^∗ and X₁ U X₂ case will introduce a dependent variable.

Reduction Step [Slide 23]

Let X,X₁ and X₂ denote non state formulae and w a state formula then the deﬁnition of past Transition formula ℛ_k(FL) is as follows:

For k ∈{0,1}

FL	ℛ_k(FL)

¬X	ℛ_k(X)
X₁ ∨X₂	ℛ_k(X₁) ∧ℛ_k(X₂)
X⟨test(W)⟩	ℛ_k(X)
X⟨pstep(PT)⟩	k = 0 : (r_{X⟨pstep(PT)⟩}≡(PT ∧ℛ′₀(X))) ∧ℛ₀(X)
	k = 1 : ℛ₀(X)
X⟨PE₁ ∨PE₂⟩	ℛ_k(X⟨PE₁⟩∨X⟨PE₂⟩)
PE₁ PE₂⟨X⟩	ℛ_k(X⟨PE₁⟩⟨PE₂⟩)
X⟨PE⟩	(r_X⟨PE⟩≡ℛ′₁(X₁)) ∧ℛ₁(X₁)
	where X₁ is X ∨r_X⟨PE⟩⟨pc(PE)⟩
X₁ S X₂	(r_X₁SX₂ ≡(ℛ′₁(X₂) ∨(ℛ′₁(X₁) ∧r_X₁SX₂))
X	ℛ_k(X⟨pstep(true)⟩)

So only the pstep(PT), FE^∗ and X₁ S X₂ case will introduce a dependent variable.

Reduction Step [Slide 24]

Let X,X₁ and X₂ denote non state formulae and w a state formula then the deﬁnition of state formula ℛ′_k(FL) is as follows:

For k ∈{0,1}

FL	ℛ′_k(FL)

W	W
⟨test(W)⟩X	W ∧ℛ′_k(X)
⟨step(FT)⟩X	k = 0 : r_{⟨step(FT)⟩X}
	k = 1 : FT ∧ℛ′₀(X)
⟨FE₁ ∨FE₂⟩X	ℛ′_k(⟨FE₁⟩X ∨⟨FE₂⟩X)
⟨FE₁ ; FE₂⟩X	ℛ′_k(⟨FE₁⟩⟨FE₂⟩X)
⟨FE^∗⟩X	r_{⟨FE^∗⟩X}
¬X	¬ℛ′_k(X)
X₁ ∨X₂	ℛ′_k(X₁) ∨ℛ′_k(X₂)
X₁ U X₂	r_X₁UX₂
X₁	ℛ′_k(⟨step(true)⟩X)

Reduction Step [Slide 25]

Let X,X₁ and X₂ denote non state formulae and w a state formula then the deﬁnition of state formula ℛ′_k(FL) is as follows:

For k ∈{0,1}

FL	ℛ′_k(FL)

X⟨test(W)⟩	W ∧ℛ′_k(X)
X⟨pstep(PT)⟩	k = 0 : r_{X⟨pstep(PT)⟩}
	k = 1 : PT ∧ℛ′₀(X)
X⟨PE₁ ∨PE₂⟩	ℛ′_k(X⟨PE₁⟩∨X⟨PE₂⟩)
X⟨PE₁ PE₂⟩	ℛ′_k(X⟨PE₁⟩⟨PE₂⟩)
X⟨PE⟩	r_X⟨PE⟩
X₁ S X₂	r_X₁SX₂
X₁	ℛ′_k(X⟨pstep(true)⟩)

Reduction Step [Slide 26]

Reduction function for ⟨FE^∗⟩X is a bit more involved because FE could be valid for intervals with only one state. Solution: a function c is introduced which transforms an arbitrary future fusion expression FE into another formula c(FE) such that c(FE) ≡ FE ∧more_r^e holds. Note: ⟨FE^∗⟩X ≡⟨c(FE)^∗⟩X holds.

FE	c(FE)

test(W)	test(¬true)
step(FT)	step(FT)
FE₁ ∨ FE₂	c(FE₁) ∨ c(FE₂)
FE₁ ; FE₂	c(FE₁) ; FE₂ ∨ FE₁ ; c(FE₂)
FE^∗	c(FE) ; FE^∗

Reduction Step [Slide 27]

Reduction function for X⟨PE⟩ is a bit more involved because PE could be valid for intervals with only one state. Solution: a function pc is introduced which transforms an arbitrary past fusion expression PE into another formula pc(PE) such that pc(PE) ≡ PE ∧more_l^e holds. Note: X⟨PE⟩X ≡ X⟨pc(PE)⟩ holds.

PE	pc(PE)

test(W)	test(¬true)
pstep(PT)	pstep(PT)
PE₁ ∨ PE₂	pc(FE₁) ∨ pc(PE₂)
PE₁ PE₂	pc(PE₁) PE₂ ∨ PE₁ pc(PE₂)
PE	PEpc(PE)

Reduction Step [Slide 28]

Transform ﬁnit ∧ T into init ∧ I

Let FL be a fusion Logic formula and dep(FL) be the dependent variables introduced by ℛ′₀(FL) and ℛ₀(FL) then

(1) FL ≡∃dep(FL) (ℛ′₀(FL) ∧ℛ₀(FL))
We know that ℛ₀(FL)) is of the form F ∧ P where:

F ≜ (∧ _i=1^kr_{X_i} ≡ FT_i) and P ≜ (∧ _j=1ⁿr_{Y _j} ≡ PT_j)

where FT_i is future transition formula and PT_j is a past transition formula
Let ﬁrst ≜¬true denote a formula which holds in the ﬁrst state of an interval.

We shift reasoning back to a starting state of a satisfying interval then FL is satisﬁable iﬀ

(2) ∃dep(FL) (ﬁrst ∧ﬁnit ∧(F ∧ P))

is satisﬁable

Reduction Step [Slide 29]

Let F′ be the future transition formula obtained from P by replacing each construct in P by its operand and by taking each state formula in P which does not occur in and enclosing it in (time reversal)
Let pinit be a state formula obtained from P by replacing each construct by false then (2) is satisﬁable iﬀ

(3) ∃dep(FL) (pinit ∧ﬁnit ∧(F ∧ (more_r ⊃ F′)))

is satisﬁable
Let r_Z be a fresh dependency (r_Z ∉ dep(FL)) then (3) is satisﬁable iﬀ

(4) ∃dep(FL) ∪{r_Z} (pinit ∧ r_Z ∧

(F ∧ (more_r ⊃ F′) ∧ (r_Z ≡ (ﬁnit ∨ r_Z))))

is satisﬁable
(4) is in the required form ∃X init ∧ I as (F ∧ (more_r ⊃ F′) ∧ (r_Z ≡ (ﬁnit ∨ r_Z))) is a future transition formula and pinit ∧ r_Z is a state formula

Example [Slide 30]

Given a future fusion logic formula

⟨step(A)^∗⟩(B ∨ C) ∨⟨step(A) ; test(B)⟩D

The Reduction Step yields:

init ≜ r_X₁ ∨ r_X₃ where X₁ ≜⟨step(A)^∗⟩(B ∨ C) and X₃ ≜⟨step(A)⟩⟨test(B)⟩D.

The corresponding invariant I is

I ≜ (r_X₁ ≡ (B ∨ C) ∨ (A ∧ r_X₁)) ∧ (r_X₃ ≡ A ∧(B ∧ D))

Example [Slide 31]

Given a past fusion logic formula

(B ∨ C) ∧ (D⟨pstep(A) test(B)⟩)

The Reduction Step yields:

ﬁnit ≜ r_X₁ ∧ (B ∧ r_X₂) where X₁ ≜(B ∨ C) and X₂ ≜ D⟨pstep(A) test(B)⟩.

The corresponding invariant PI is

PI ≜ (r_X₁ ≡(B ∨ C)) ∧ (r_X₂ ≡ A ∧ D)

This is transformed into

init ≜ (r_X₁ ≡false) ∧ (r_X₂ ≡ A ∧false) ∧ r_Z

I ≜ (r_Z ≡ (ﬁnit ∨ r_Z)) ∧ (more_r ⊃ ((( r_X₁) ≡ (B ∨ C)) ∧ (( r_X₂) ≡ ( A) ∧ D)))

4.2 BDD Step

BDD Step [Slide 32]

Transform init ∧ I into BDD based satisﬁability problem.

init: a state formula

I: an invariant, ∧ _i=1^k(FT_i) (for k ≥ 1) where

where FT_i contains dependent variable r_{X_i} and

FT_i is a future transition formula

Let us examine the ‘Always’ operator

init ∧ I	●	●	●	●	●
					⟨I⟩
				⟨—I—⟩
			⟨—I—	— —⟩
		⟨—I—	— —	— —⟩
	⟨—I—	— —	— —	— —⟩
	init

BDD Step [Slide 33]

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 ∧ I	●	●	●	●	●
					⟨I⟩
				⟨—I—⟩
			⟨—I—⟩
		⟨—I—⟩
	⟨—I—⟩
	init

BDD Step [Slide 34]

Introducing BDDs Γ_i’s:

Γ₁ represents the state formula init.
Γ₂ 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 .
Γ₃ captures the behaviour of invariant I in an interval with only 1 state. This can be done by replacing each construct by false.
Γ₄ ≜ﬁnit if the original formula FL contains past time operators and ﬁnit is obtained from (r_Z ≡ (ﬁnit ∨ r_Z)) and if the original formula FL contains no past time operators then Γ₄ ≜ Γ₁

init ∧ I	●	●	●	●	●
					Γ₃
				⟨—Γ₂—⟩
			⟨—Γ₂—⟩
		⟨—Γ₂—⟩
	⟨—Γ₂—⟩
	Γ₁

Example [Slide 35]

Given right fusion logic formula

⟨step(A)^∗⟩(B ∨ C) ∨⟨step(A) ; test(B)⟩D

With Init = r_X₁ ∨ r_X₃ and corresponding invariant:

I = (r_X₁ ≡ (B ∨ C) ∨ (A ∧ r_X₁)) ∧ (r_X₃ ≡ A ∧(B ∧ D))

Then Γ₁ = r_X₁ ∨ r_X₃ and

Γ₂ = (r_X₁ ≡ (B ∨ C) ∨ (A ∧ r′_X₁)) ∧ (r_X₃ ≡ A ∧ (B′∧ D′))

and

Γ₃ = (r_X₁ ≡ (B ∨ C) ∨ (A ∧false)) ∧ (r_X₃ ≡ A ∧false)

BDD Step [Slide 36]

Encoding as a BDD-based satisﬁability problem:

We use Γ₂ and Γ₁ to iteratively calculate a sequence of BDDs Δ₀,…,Δ_n, so that for any n, Δ_n described all states which can be reached from Γ₁ in exactly n steps using Γ₂.
We determine at each iteration whether BDD Γ₃ ∧ Δ_n is true or not. If false we must continue to iterate and if true then there is exists some state satisfying Γ₃ which can be reached in n steps from Γ₁, so we can stop the iteration, i.e., original FL 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 Γ₁. 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 Γ₃ then original FL is not satisﬁable.

BDD Step [Slide 37]

To construct a satisfying interval (in case FL is satisﬁable) we proceed as follows.

Let Δ_m be that set of states for which Γ₃ ∧ Δ_m is true.

If there are no independent variables (only r_i variables) then any interval of length m will satisfy FL.
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 Γ₂ to state σ_m (weakest precondition of Γ₂ and σ_m). Again choose one state σ_m−1 of Pr_m−1.

Continue until we reach Pr₀ and then choose state σ₀.

The states σ₀…σ_m−1σ_m will then represent a (minimal) satisfying interval σ for FL.
To determine the current state we check whether a state in this satisfying interval satisﬁes Γ₄.

Implementation [Slide 38]

Implementation of decision procedure

References [Slide 39]

2025-12-19