STRL
© 1996-2015







4 Decision Procedure for Fusion Logic

  • 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 BDD-based satisfiability problem

4.1 Time Reversal Step

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

  • Let   r
F denotes the time reversed version of fusion logic formula F .
  • Let reverse(σ) denote the time reversed interval of σ :
    reverse(σ0 ...σ|σ|) ^= σ|σ|...σ0

  • ⟦Fr⟧σ = ttiff ⟦F⟧reverse(σ) = tt

Rules to rewrite left fusion logic formulae into right fusion logic formulae

leftfusionformulae             |
-----⟨---⟩-------⟨-----⟩----|
 ((L  E   )r  =    Er   Lr  |
 (fin(p))r     =  p          |
 truer         =  true        |
 ( L)r       =   (Lr)     |
-(L1-∨-L2)r---=--Lr1 ∨-Lr2------------------------------
fusionexpressions              |transitions
--------------------------  |-------------------------
 (test(W ))r  =   test(W )    | (○W  )r    =   W
 (step (T ))r  =   step(T r)   | W r        =   ○W
 (E1 ∨ E2)r  =   Er1 ∨ Er2    | (T1 ∨ T2 )r =  Tr1 ∨ Tr2
 (E1 ;E2)r   =   Er2 ;Er1     | ( T)r     =   (T r)
 (E *)r       =   (Er )*      |

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              r
⟦L⟧σ = ttiff ⟦L ⟧reverse(σ) = tt

4.2 Reduction Step

Transform right fusion logic formula R into an equivalent reduced form init ∧ !r I where

  • init : a state formula
    init=^ R ′(f )
         0

  • I : an invariant, ∧
  ii==k1(rXi ≡ ti) (for k ≥ 1 ) where
    rX
  i  is a dependent Boolean variable (not appearing in F )
    ti is a transition formula
    I ^= R0 (f)

Let X, X1  and X2  denote non state formulae and w a state formula then the definition of Transition formula Rk (f) is as follows:

For k ∈ {0,1}

R             |Rk (R )
W-------------|true-----------------------------------------
⟨⟨ test(W  ) ⟩⟩ X |Rk (X )
  step(T)  X   |k = 0 : (r⟨ step(T) ⟩X ≡ (T ∧ ○R ′0(X ))) ∧ R0(X )
              |k = 1 : R0 (X )
⟨⟨ E1 ∨ E2 ⟩⟩X |Rk (⟨⟨ E1 ⟩⟩ X⟨ ∨ ⟨ E⟩2 ⟩X )
⟨ E1 ;⟩E2  X   |Rk ( E1    E2   X )
  E*  X       |(r⟨ E * ⟩X ≡ R ′1(X1)) ∧ R1 (X1)
              |where X1 isX ∨ ⟨ c(E) ⟩r⟨ E* ⟩X
 X           |Rk (X )
X1 ∨ X2       |Rk (X1 ) ∧ R0 (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  ′
Rk(f ) is as follows:

For k ∈ {0,1}

              ||
-R------------||R-′k(R-)------------------
 W⟨        ⟩   ||W
 ⟨ test(W  )⟩ X ||W  ∧ R ′k(X )
   step(T)  X  ||k = 0 : r⟨ step(T) ⟩X
 ⟨         ⟩  ||k =⟨1 : T ∧⟩ ○R ′0(⟨X ) ⟩
 ⟨ E1 ∨ E2 ⟩ X||R ′k′(⟨ E1 ⟩ X⟨ ∨  E⟩2   X )
 ⟨ E1* ;⟩E2  X  ||R k( E1    E2   X )
   E   X      ||r⟨ E* ⟩X
  X          || R′′k(X )   ′
 X1 ∨ X2        R k(X1 ) ∨ R 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 ∧ m oree holds. Note: ⟨    ⟩      ⟨       ⟩
  E*   W  ≡   c(E)*  W holds.

          |
-------E--|c(E)------------------
  test(W  ) |te st( true)
  step(T ) |ste p(T )
 E1 ∨ E2  |c(E1) ∨ 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 R ′(R)
  k and R  (R)
  k (k = 0,1 ) then
                 o   ′
R ≡ ∃dep (R)  (R k(R ) ∧ ! Rk (R))

Given a right fusion logic formula

⟨ ste p(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 = (rX  ≡  (B  ∨ C) ∨ (A ∧ ○rX  )) ∧ (rX  ≡  A ∧ ○(B ∧ D ))
        1                      1       3

4.3 BDD Step

Transform init ∧ !r I into BDD based satisfiability problem.

init : a state formula
I : an invariant, ∧i=k
 i=1(rXi ≡ ti) (for k ≥ 1 ) where
rX
   i  is a dependent variable and
ti 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 first two states of each suffix interval.

init ∧ !r I ∙     ∙      ∙      ∙      ∙
                                      ⟨I⟩
                                ⟨—I —⟩
                         ⟨—I — ⟩
                  ⟨—I — ⟩
            ⟨—I — ⟩
            init

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 itlC 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

Given right fusion logic formula

⟨ ste p(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:

  • 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 satisfiable.
  • 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 find a state that satisfies Γ 3  then original f is not satisfiable.

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 no independent variables (only ri 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 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 Pr m- 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