Decision Procedure for Fusion Logic

4 Decision Procedure for Fusion Logic

4.1 Time Reversal Step
4.2 Reduction Step
4.3 BDD Step

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

4.1 Time Reversal Step

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(σ₀…σ_|σ|) ≜ σ_|σ|…σ₀
M⟦Fr⟧(σ) = 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	=	⟨Er⟩Lr
(ﬁn(p))r	=	p
truer	=	true
(¬L)r	=	¬(Lr)
(L₁ ∨ L₂)r	=	L₁r ∨ L₂r

fusion expressions

transitions


(test(W))r	=	test(W)
(step(T))r	=	step(Tr)
(E₁ ∨ E₂)r	=	E₁r ∨ E₂r
(E₁ ; E₂)r	=	E₂r ; E₁r
(E^∗)r	=	(Er)^∗


( W)r	=	W
Wr	=	W
(T₁ ∨ T₂)r	=	T₁r ∨ T₂r
(¬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 M⟦ L⟧(σ) = tt iﬀ M⟦Lr⟧(reverse(σ)) = tt

4.2 Reduction Step

Reduction Step [Slide 21]

Transform right fusion logic formula R into an equivalent reduced form init ∧_rI where

init: a state formula

init ≜ℛ′₀(f)
I: an invariant, ∧ _i=1^i=k(r_{X_i} ≡ t_i) (for k ≥ 1) where

r_{X_i} is a dependent Boolean variable (not appearing in F)
t_i is a transition formula

I ≜ℛ₀(f)

Reduction Step [Slide 22]

Let X,X₁ and X₂ 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 ∧ℛ′₀(X))) ∧ℛ₀(X)
	k = 1 : ℛ₀(X)
⟨E₁ ∨E₂⟩X	ℛ_k(⟨E₁⟩X ∨⟨E₂⟩X)
⟨E₁ ; E₂⟩X	ℛ_k(⟨E₁⟩⟨E₂⟩X)
⟨E^∗⟩X	(r_⟨E^∗⟩X ≡ℛ′₁(X₁)) ∧ℛ₁(X₁)
	where X₁ is X ∨⟨c(E)⟩r_⟨E^∗⟩X
¬X	ℛ_k(X)
X₁ ∨X₂	ℛ_k(X₁) ∧ℛ₀(X₂)

So only the step(t) and e^∗ 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 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 ∧ℛ′₀(X)
⟨E₁ ∨E₂⟩X	ℛ′_k(⟨E₁⟩X ∨⟨E₂⟩X)
⟨E₁ ; E₂⟩X	ℛ′_k(⟨E₁⟩⟨E₂⟩X)
⟨E^∗⟩X	r_⟨E^∗⟩X
¬X	¬ℛ′_k(X)
X₁ ∨X₂	ℛ′_k(X₁) ∨ℛ′_k(X₂)

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₁ ∨ E₂	c(E₁) ∨ c(E₂)
E₁ ; E₂	c(E₁) ; E₂ ∨ E₁ ; c(E₂)
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_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))

4.3 BDD Step

BDD Step [Slide 27]

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

init: a state formula

I: an invariant, ∧ _i=1^i=k(r_{X_i} ≡ t_i) (for k ≥ 1) where

r_{X_i} is a dependent variable and

t_i 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:

Γ₁ 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, i.e., ¬true.

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

Example [Slide 30]

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 31]

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 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 Γ₁. 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 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 Γ₃ ∧ Δ_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 Γ₂ 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 F.

Implementation [Slide 33]

Implementation of decision procedure

2024-08-02