ITL
© 1996-2018







3 Fusion Logic

3.1 Syntax

Syntax of Fusion Logic [Slide 4]

State formulae:

W ::=
true|p|W1 W2|¬W

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

Left Fusion logic formulae:

L ::=
true|fin(p) |¬L|L1 L2|LE

Fusion logic formulae:

F ::=
L|R

3.2 Semantics

State [Slide 5]

A state is a mapping State from the set of propositional variables Varb to the set of Boolean values Bool {tt,}.

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

State : Varb Bool

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

Example 1. Let σ0 be a state such that

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

Interval and Length [Slide 6]

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
σ = σ0σ1
|σ| = 1
σ = σ0σ1σn
|σ| = n

Prefix, Suffix and Sub Interval [Slide 7]

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

  • σ0σk(where 0 k |σ|) denotes a prefix interval of σ
  • σkσ|σ|(where 0 k |σ|) denotes a suffix interval of σ
  • σkσl(where 0 k l |σ|) denotes a sub interval of σ

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

σ0σ1
is a prefix interval of σ
σ1σ2σ3
is a suffix interval of σ
σ1σ2
is a sub interval of σ

Semantics of State Formula [Slide 8]

Let M be the “meaning” function from ‘state formulae’ × Σ+ to {tt,} and let σ be a finite interval (σ Σ+) then

Mtrue(σ)
=
tt
Mp(σ)
=
σ0(p)
M¬W(σ)
=
not MW(σ)
MW1 W2(σ)
=
MW1(σ) or MW2(σ)

Semantics of Transition formulae [Slide 9]

Let M be the “meaning” function from ‘transition formulae’ × Σ+ to {tt,} and let σ be a finite interval (σ Σ+) then

M¬T(σ)
=
not MT(σ)
MT1 T2(σ)
=
MT1(σ) or MT2(σ)
MW(σ)
=
MW(σ 1σ|σ|) and |σ| > 0

Semantics of Fusion expressions [Slide 10]

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

Mtest(W)(σ)
=
MW(σ0) and |σ| = 0
Mstep(T)(σ)
=
MT(σ0σ1) and |σ| = 1
ME1 E2(σ)
=
ME1(σ) or ME2(σ)
ME0 ; E1(σ) = tt
iff
exists a k, s.t. 0 k |σ| and
ME0(σ0σk) = tt and ME1(σkσ|σ|) = tt
ME(σ) = tt
iff
exist l0,,ln s.t. l0 = 0 and ln = |σ| and
for all 0 i < n,li < li+1 and
ME(σliσli+1) = tt

Semantics of right Fusion logic [Slide 11]

Let M be the “meaning” function from ‘right fusion logic formulae’ × Σ+ to {tt,} and let σ be a finite interval (σ Σ+) then

M¬R(σ) =
=
not MR(σ)
MR1 R2(σ)
=
MR1(σ) or MR2(σ)
MER(σ) = tt
iff
exists a k, s.t. 0 k |σ| and
ME(σ0σk) = tt and
MR(σkσ|σ|) = tt

Semantics of left Fusion logic [Slide 12]

Let M be the “meaning” function from ‘left fusion logic formulae’ × Σ+ to {tt,} and let σ be a finite interval (σ Σ+) then

Mfin(p)(σ)
=
σ|σ|(p)
M¬L(σ)
=
not ML(σ)
ML1 L2(σ)
=
ML1(σ) or ML2(σ)
MLE(σ) = tt
iff
exists a k, s.t. 0 k |σ| and
ML(σ0σk) = tt and
ME(σkσ|σ|) = tt

Derived operators [Slide 13]

Derived Fusion expression operators

lene(0)
test(true)
lene(n + 1)
step(true) ; lene(n)
truee
step(true)
moree
step(true) ; truee
eW
truee ; test(W) ; truee
eW
step(W) ; test(W)
n : W
truee ; test(W) ; lene(n)

Derived operators [Slide 14]

Derived right Fusion logic operators

R1 R2
¬(¬R1 ¬R2)
R1 R2
¬R1 R2
morer
step(true)true
emptyr
¬morer
lenr(0)
emptyr
lenr(n + 1)
step(true)lenr(n)
rR
trueeR
rR
¬r(¬R)
rT
rstep(T)true
rW
rtrueetest(W)true
rW
¬r(¬W)
n : rW
trueetest(W)lenr(n)
[E]R
¬(E¬R)

Derived operators [Slide 15]

Derived left Fusion logic operators

L1 L2
¬(¬L1 ¬L2)
L1 L2
¬L1 L2
morel
truestep(true)
emptyl
¬morel
lenl(0)
emptyl
lenl(n + 1)
lenl(n)step(true)
lW
truetest(W)truee
lW
¬l(¬W)
lL
Ltruee
lL
¬l(¬L)
n : lW
truetest(W)lene(n)
L[E]
¬(¬LE)

Satisfiable and valid [Slide 16]

  • A fusion logic formula F is satisfiable if and only if there exists an interval σ such that MF(σ) = 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 σ, MF(σ) = 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







2018-02-25
Contact | Home | ITL home | Course | Proofs | Algebra | FL