STRL
© 1996-2015







3 Fusion Logic

3.1 Syntax

State formulae:

W  ::=   true|p|W  ∨ W  | W
                1    2

Transition formulae:

T  ::=  W  |○W  |T1 ∨ T2| T

Fusion expressions:

E ::=   test(W )|step(T)|E1 ∨ E2|E1 ;E2|E *

Right Fusion logic formulae:

                          ⟨   ⟩
R ::=   true|p| R |R1  ∨ R2 | E   R

Left Fusion logic formulae:

L ::=  true|fin(p )| L|L1 ∨ L2|L⟨ E  ⟩

Fusion logic formulae:

F ::=  L |R

3.2 Semantics

A state is a mapping State from the set of propositional variables V arb to the set of Boolean values Bool  ^= {tt,ff} .

tt  is the semantic ‘true’ value and ff  the semantic ‘false’ value.

State : Varb → Bool

We will use σ0,σ1, σ2,... to denote states and Σ to denote the set of all possible states.

Example 1 Let σ0  be a state such that

σ (P ) = tt
σ0(Q ) = ff
 0

_____________________________________________________________________

An interval σ is a finite sequence of states

σ : σ0 σ1σ2...

Let Σ+  denote the set of all possible finite intervals with at least one state.

The length of an interval σ is denoted by |σ| and is the number of states minus 1.

Example 2

σ = σ           |σ| = 0
σ = σ0σ         |σ| = 1
σ = σ0σ 1...σ   |σ| = n
     0  1    n

_____________________________________________________________________

Let σ =  σ0σ1σ2 ... be an interval then

  • σ0 ...σk(where0 ≤ k ≤ |σ|) denotes a prefix interval of σ
  • σk ...σ|σ |(where0 ≤ k ≤ |σ|) denotes a suffix interval of σ
  • σk ...σl(w here 0 ≤ k ≤ l ≤ |σ|) denotes a sub interval of σ

Example 3 Let σ =  σ0σ1σ2σ3  be an interval then

σ0σ1     isa prefixintervalofσ
σ1σ2 σ3  isa suffi xintervalofσ
σ1σ2     isa sub intervalofσ

_____________________________________________________________________

Let ⟦⟧ be the “meaning” function from ‘stateformulae’×  Σ+  to {tt,ff} and let σ be a finite interval (σ ∈ Σ+  ) then

⟦true⟧σ       =   tt
⟦p⟧σ         =   σ0(p)
⟦ W ⟧σ      =   not⟦W ⟧σ
⟦W1  ∨ W2 ⟧σ =   ⟦W1 ⟧σ or⟦W2 ⟧σ

Let ⟦⟧ be the “meaning” function from ‘transitionform ulae’× Σ+  to {tt,ff} and let σ be a finite interval (σ ∈ Σ+  ) then

⟦T ⟧σ     =   not⟦T ⟧σ
⟦T1 ∨ T2⟧σ =   ⟦T1⟧σ or⟦T2⟧σ
⟦○W  ⟧σ    =   ⟦W ⟧σ1...σ|σ| and |σ | > 0

Let ⟦⟧ be the “meaning” function from                    +
‘fusion expressions’× Σ  to {tt,ff } and let σ be a finite interval (      +
σ ∈ Σ  ) then

⟦test(W )⟧    =    ⟦W  ⟧  and|σ| = 0
⟦step(T )⟧σ   =    ⟦T ⟧σ0   and |σ | = 1
⟦E  ∨ E σ⟧    =    ⟦E  σ⟧0...oσr1⟦E  ⟧
⟦E1 ;E 2⟧ σ= ttiff   exi1stsσa k, s.t2.σ0 ≤ k ≤ |σ|and
  0    1σ         ⟦E  ⟧     =  ttand ⟦E  ⟧       = tt
   *                0 σ0...σk          1 σk...σ|σ|
⟦E ⟧σ = tt   iff   existl0,...,ln s.t.l0 = 0andln = |σ|and
                  forall0 ≤ i < n, li < li+1 and⟦E ⟧σli...σli+1 = tt

Let ⟦⟧ be the “meaning” function from ‘rightfusion logicform ulae’× Σ+  to {tt,ff} and let σ be a finite interval (σ ∈ Σ+  ) then

⟦R ⟧σ =        =  not⟦R ⟧σ
⟦R⟨1 ∨⟩R2⟧σ      =  ⟦R1 ⟧σ or⟦R2 ⟧σ
⟦ E   R ⟧σ = tt  iff  existsa k, s.t. 0 ≤ k ≤ |σ|and
                   ⟦E ⟧σ0...σk = ttand ⟦R ⟧σk...σ|σ| = tt

Let ⟦⟧ be the “meaning” function from ‘leftfusion logicform ulae’× Σ+  to {tt,ff} and let σ be a finite interval (σ ∈ Σ+  ) then

⟦fin(p)⟧σ         =  σ |σ|(p)
⟦ L⟧σ          =  not⟦L ⟧σ
⟦L1⟨∨ L2⟩⟧σ      =  ⟦L1 ⟧σ or⟦L2⟧σ
⟦L   E  ⟧σ = tt  iff  existsa k, s.t. 0 ≤ k ≤ |σ|and
                   ⟦L ⟧σ0...σk = ttand⟦E ⟧σk...σ|σ| = tt

Derived Fusion expression operators

len (0 )     =^  te st(true)
lene(n + 1 ) =^  step (true);len (n )
truee        =^  step (true)*   e
m oere        =^  step (true);true
   We       =^  true  ;test(W )e; true
! eW        =^  stepe(W  )* ;test(W ) e
n e: W       =^  true  ;test(W ); len (n)
                   e             e

Derived right Fusion logic operators

R1 ∧ R2     ^=   ( R1 ∨ R2 )
R1 ⊃ R2     ^=  ⟨ R1  ∨ R2  ⟩
morer       ^=    step(true)  true
emptyr      ^=   m orer
lenr(0)      ^=  e⟨ mptyr     ⟩
lenr(n + 1)  ^=  ⟨ step(tru⟩e)  lenr(n )
 r R        ^=    truee  R
!r R        ^=    ⟨r(R )   ⟩
!r T        ^=  !r ⟨ step(T⟩)⟨ true     ⟩
i r W       ^=  !r   truee    test(W  )  true
!i r W       ^=  ⟨  i r( W⟩⟨)       ⟩
n[ :r W]       ^=    tr⟨uee⟩   test(W )  lenr(n )
 E   R      ^=   (  E   R )

Derived left Fusion logic operators

L1 ∧ L2     ^=   ( L1 ∨  L2)
L1 ⊃  L2    ^=    L1⟨ ∨ L2      ⟩
m orel      ^=   true  step(true)
em ptyl      ^=    morel
lenl(0)      ^=   emptyl⟨           ⟩
lenl(n + 1)  ^=   lenl(⟨n)  step(tr⟩ue⟨)     ⟩
  lW        ^=   true  test(W  )    truee
!l W        ^=    ⟨l(W  )⟩
 i lL       ^=   L  truee
!i lL       ^=    i l⟨( L )   ⟩ ⟨        ⟩
n :[l W ]    ^=   true  te⟨st(W⟩ )    lene(n)
L   E       ^=   ( L   E  )

  • A fusion logic formula F is satisfiable if and only if there exists an interval σ such that ⟦F ⟧σ =  tt
  • Decision procedure checks whether F is satisfiable or not, when F is satisfiable a satisfying interval is generated.
  • A fusion logic formula F is valid if and only if for all intervals σ , ⟦F ⟧σ = tt
  • F is not valid if and only if F is satisfiable i.e., satisfying interval for  F will represent a counter example for F ’s validity F is valid if and only if  F is not satisfiable