State formulae:
W ::= | true | p | W1 ∨ W2 |¬W |
Future Transition formulae:
FT ::= | W | W | FT1 ∨ FT2 |¬FT |
Past Transition formulae:
PT ::= | W | W | PT1 ∨ PT2 |¬PT |
Future Fusion expressions:
FE ::= | test(W) |step(FT) | FE1 ∨ FE2 | FE1 ; FE2 | FE∗ |
Past Fusion expressions:
PE ::= | test(W) |pstep(PT) | PE1 ∨ PE2 | PE1 PE2 | PE |
Fusion logic formulae:
FL ::= | true | p |¬FL | FL1 ∨ FL2 | FL | FL | |
⟨FE⟩FL | FL⟨PE⟩| FL1 U FL2 | FL1 S FL2 |
A state is a mapping State from the set of propositional variables Varb 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.
An interval σ is a finite sequence of states, in [5] also infinite intervals are considered. The decision procedure can also handle infinite intervals.
σ : σ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.
Let σ = σ0σ1σ2… be an interval then
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 σ |
Let P⟦⟧() be the “meaning” function from ‘state formulae’ × Σ to {tt,ff} and let σ be a finite interval of one state then
P⟦true⟧(σ) |
= |
tt |
P⟦p⟧(σ) | = | σ0(p) |
P⟦¬W⟧(σ) | = | not P⟦W⟧(σ) |
P⟦W1 ∨ W2⟧(σ) |
= |
P⟦W1⟧(σ) or P⟦W2⟧(σ) |
Let Tf⟦⟧() and Tp⟦⟧() be the “meaning” function from respectively ‘future transition formulae’ × Σ2 to {tt,ff} and ‘past transition formulae’ × Σ2 to {tt,ff} and let σ be a finite interval (σ ∈ Σ2) with two states then
future transitions:
Tf⟦¬FT⟧(σ) |
= |
not Tf⟦FT⟧(σ) |
Tf⟦FT1 ∨ FT2⟧(σ) |
= |
Tf⟦FT1⟧(σ) or Tf⟦FT2⟧(σ) |
Tf⟦W⟧(σ) | = | P⟦W⟧(σ0) |
Tf⟦ W⟧(σ) |
= |
P⟦W⟧(σ1) |
past transitions:
Tp⟦¬PT⟧(σ) |
= |
not Tp⟦PT⟧(σ) |
Tp⟦PT1 ∨ PT2⟧(σ) |
= |
Tp⟦PT1⟧(σ) or Tp⟦PT2⟧(σ) |
Tp⟦W⟧(σ) | = | P⟦W⟧(σ1) |
Tp⟦ W⟧(σ) |
= |
P⟦W⟧(σ0) |
Let E⟦⟧() be the “meaning” function from ‘future fusion expressions’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
E⟦test(W)⟧(σ) |
= |
P⟦W⟧(σ0) and |σ| = 0 |
E⟦step(FT)⟧(σ) |
= |
Tf⟦FT⟧(σ0…σ1) and |σ| = 1 |
E⟦FE1 ∨ FE2⟧(σ) |
= |
E⟦FE1⟧(σ) or E⟦FE2⟧(σ) |
E⟦FE1 ; FE2⟧(σ) = tt |
iff |
|
exists a k, s.t. 0 ≤ k ≤|σ| and |
||
E⟦FE1⟧(σ0…σk) = tt and |
||
E⟦FE
2⟧(σk…σ|σ|) = tt |
||
E⟦FE∗⟧(σ) = tt |
iff |
|
exist l0,…,ln s.t. l0 = 0 and ln = |σ| and |
||
for all 0 ≤ j < n,lj < lj+1 and |
||
E⟦FE⟧(σli…σlj+1) = tt |
||
The semantics of ; and ∗ are the same as those of ITL
Let E⟦⟧() be the “meaning” function from ‘past fusion expressions’ × Σ+ to {tt,ff} and let σ be a finite interval (σ ∈ Σ+) then
E⟦test(W)⟧(σ) |
= |
P⟦W⟧(σ0) and |σ| = 0 |
E⟦pstep(PT)⟧(σ) |
= |
Tp⟦PT⟧(σ0…σ1) and |σ| = 1 |
E⟦PE1 ∨ PE2⟧(σ) |
= |
E⟦PE1⟧(σ) or E⟦PE2⟧(σ) |
E⟦PE1 PE2⟧(σ) = tt |
iff |
|
exists a k, s.t. k ≤ i and |
||
E⟦PE1⟧(σ0…σk) = tt and |
||
E⟦PE2⟧(σk…σ|σ|) = tt |
||
E⟦PE⟧(σ) = tt |
iff |
|
exist l0,…,ln s.t. l0 = 0 and ln = |σ| and |
||
for all 0 ≤ j < n,lj < lj+1 and |
||
E⟦PE⟧(σlj…σlj+1) = tt |
||
The semantics of and are the same as ; and ∗
Let M⟦⟧ be the “meaning” function from ‘fusion logic formulae’ × Σ+ ×IN to {tt,ff} and let σ be a finite interval and i a natural number then
M⟦true⟧(σ,i) |
= |
tt |
M⟦p⟧(σ,i) |
= |
σi(p) |
M⟦¬FL⟧(σ,i) = |
= |
not M⟦FL⟧(σ,i) |
M⟦FL1 ∨ FL2⟧(σ,i) | = | M⟦FL1⟧(σ,i) or M⟦FL2⟧(σ,i) |
M⟦ FL⟧(σ,i) |
= |
M⟦FL⟧(σ,i + 1) and i < |σ| |
M⟦ FL⟧(σ,i) |
= |
M⟦FL⟧(σ,i − 1) and 0 < i |
M⟦⟨FE⟩FL⟧(σ,i) = tt |
iff |
exists a k, s.t. i ≤ k ≤|σ| and |
E⟦FE⟧(σi…σk) = tt and |
||
M⟦FL⟧(σ,k) = tt |
||
M⟦FL⟨PE⟩⟧(σ,i) = tt |
iff |
exists a k, s.t. k ≤ i and |
M⟦FL⟧(σ,k) = tt and |
||
E⟦PE⟧(σk…σi) = tt |
||
M⟦FL1 U FL2⟧(σ,i) = tt | iff | exists a k, s.t. i ≤ k ≤|σ| and |
M⟦FL2⟧(σ,k) = tt and |
||
for all i ≤ j < k,M⟦FL1⟧(σ,j) = tt |
||
M⟦FL1 S FL2⟧(σ,i) = tt |
iff |
exists a k, s.t. k ≤ i and |
M⟦FL2⟧(σ,k) = tt and |
||
for all k < j ≤ i,M⟦FL1⟧(σ,j) = tt |
||
non-strict U and S see [4]
⟨FE⟩FL and FL⟨PE⟩ are similar to ; and of [1]:
M⟦⟨FE⟩FL⟧(σ,i) = tt |
iff |
exists a k, s.t. i ≤ k ≤|σ| and |
E⟦FE⟧(σi…σk) = tt and |
||
M⟦FL⟧(σ,k) = tt |
||
M⟦FL⟨PE⟩⟧(σ,i) = tt | iff | exists a k, s.t. k ≤ i and |
M⟦FL⟧(σ,k) = tt and |
||
E⟦PE⟧(σk…σi) = tt |
||
M⟦FL1 ; FL2⟧(σ,i) = tt |
iff |
exists a k, s.t. i ≤ k ≤|σ| and |
M⟦FL1⟧(σ0…σk,i) = tt and |
||
M⟦FL2⟧(σ,k) = tt |
||
M⟦FL1 FL2⟧(σ,i) = tt | iff | exists a k, s.t. k ≤ i and |
M⟦FL1⟧(σ,k) = tt and |
||
M⟦FL2⟧(σk…σ|σ|,i − k) = tt |
||
Difference of E⟦FE⟧(σi…σk) = tt is because FE is a future fusion expression and therefore can not refer to states before state σi
Difference of E⟦PE⟧(σk…σi) = tt is because PE is a past fusion expression and therefore can not refer to states after state σi
Derived future Fusion expression operators
lener(0) |
≜ |
test(true) |
lener(n + 1) |
≜ |
step(true) ; lener(n) |
trueer | ≜ | step(true)∗ |
moreer |
≜ |
step(true) ; trueer |
erW |
≜ |
trueer ; test(W) ; trueer |
Derived past Fusion expression operators
lenel(0) |
≜ |
test(true) |
lenel(n + 1) |
≜ |
lenel(n) pstep(true) |
trueel | ≜ | pstep(true) |
moreel |
≜ |
trueel pstep(true) |
elW |
≜ |
trueel test(W) trueel |
Derived Boolean operators
FL1 ∧ FL2 |
≜ |
¬(¬FL1 ∨¬FL2) |
FL1 ⊃ FL2 | ≜ | ¬FL1 ∨ FL2 |
FL1 ≡ FL2 |
≜ |
(FL1 ⊃ FL2) ∧ (FL2 ⊃ FL1) |
Derived future Fusion logic operators
morer |
≜ |
true |
emptyr |
≜ |
¬morer |
lenr(0) |
≜ |
emptyr |
lenr(n + 1) | ≜ | ⟨step(true)⟩lenr(n) |
FL |
≜ |
true U FL |
FL |
≜ |
¬(¬FL) |
[FE]FL |
≜ |
¬(⟨FE⟩¬FL) |
Derived past Fusion logic operators
morel |
≜ |
true |
emptyl |
≜ |
¬morel |
first |
≜ |
emptyl |
lenl(0) |
≜ |
emptyl |
lenl(n + 1) |
≜ |
lenl(n)⟨pstep(true)⟩ |
FL | ≜ | true S FL |
FL |
≜ |
¬(¬FL) |
FL[PE] |
≜ |
¬(¬FL⟨PE⟩) |
FL |
≜ |
FL |
FL |
≜ |
FL |