We need a logic to rigorously describe the behaviour of systems. What is a behaviour?
Typical week in August in England:
☼, ⛈, ⛈, ☼, ☼, ⛈, ⛈ | ☺, ☹, ☹, ☺, ☺, ☹, ☹ |
Let
R ≜⛈, | ¬R ≜☼, | B ≜ ☺, | ¬B ≜ ☹. |
Then we have following behaviour
● | ● | ● | ● | ● | ● | ● |
¬R, B | R, ¬B | R, ¬B | ¬R, B | ¬R, B | R, ¬B | R, ¬B |
How to formally describe/specify a behaviour of a system?
skip
any sequence (interval) of exactly two states (snapshots)
● | ● |
One can combine skip with a Boolean operator for example:
Q ∧skip: any sequence (interval) of exactly two states such that in the first state Q holds
● |
● |
Q |
|
What if you only got Q as formula?
Q: any interval of states such that in the first state Q holds. The length of the interval is unconstrained.
● |
… |
Q |
|
What if the formula is just true?
true: any interval of states of any length (finite and contains at least 1 state). The length of the interval is unconstrained and the states within the interval are also unconstrained.
● | … |
; (chop)
concatenate (fuse) two intervals together such that the last state of the first interval is the same as first state of the second interval.
(Next)
f holds from the next state onwards, f ≜skip ; f.
(Q ∧skip) using the definition: skip ; (Q ∧skip)
skip : | ● | ● | |
Q ∧skip : |
● |
● |
|
Q |
|||
skip ; (Q ∧skip) : |
● |
● |
● |
Q |
|||
more
interval with at least two states, more ≜ true.
more : | ● | ● | … |
empty
interval with only one state, empty ≜ ¬more.
empty : | ● |
(Weak Next)
either an interval of only one state or f holds from the next state onwards, f ≜empty ∨ f.
(Q ∧ skip) is equal to, using the definition, empty ∨ (Q ∧ skip) and thus to
empty : | ● | ||
(Q ∧skip) : |
● |
● |
● |
Q |
|||
∗ (chopstar)
Finite number of fusion of intervals.
(Q ∧skip)∗:
Fuse a finite number of times an interval satisfying (Q ∧skip).
Interval satisfying Q ∧skip:
Q ∧skip : | ● | ● |
Q |
||
0 times fusion:
Q ∧skip : | ● | ● |
Q |
||
(Q ∧skip)0 : |
● |
|
Interval contains only 1 unconstrained state.
1 time fusion:
Q ∧skip : | ● | ● |
Q |
||
(Q ∧skip)1 : |
● |
● |
Q |
||
2 times fusion:
Q ∧skip : | ● | ● | |
Q |
|||
Q ∧skip : |
● |
● |
|
Q |
|||
(Q ∧skip)2 : |
● |
● |
● |
Q |
Q |
||
n times fusion:
(Q ∧skip)n : | ● | ● | … | ● | ● |
Q |
Q |
… |
Q |
||
(sometimes)
there exists a suffix interval for which f holds, f ≜true ; f
The suffix intervals of σ are:
σ2 |
σ1σ2 |
σ0σ1σ2 |
(Q): there exists a suffix interval for which Q holds
We already know: Q holds for an interval iff Q is true in the first state of that interval.
So (Q) means there exists a suffix interval σ′ such that Q is true in the first state of σ′.
Let σ ≜ σ0σ1σ2 then σ satisfies (Q) iff there exists a suffix interval σ′ (of σ) such that Q is true in the first state of σ′.
σ′ = |
σ2 |
|||
● |
no | |||
¬Q |
||||
σ′ = |
σ1 |
σ2 |
||
● |
● |
yes |
||
Q |
||||
σ′ = | σ0 | σ1 | σ2 |
|
● | ● | ● | no |
|
¬Q |
||||
σ = |
σ0 |
σ1 |
σ2 |
|
● |
● |
● | ||
¬Q |
Q |
¬Q |
||
Are there any other intervals σ ≜ σ0σ1σ2 that satisfy (Q)?
(always)
for each suffix interval f holds, f ≜¬¬f
The suffix intervals of σ are:
σ3 |
σ2σ3 |
σ1σ2σ3 |
σ0σ1σ2σ3 |
(Q): for each suffix interval Q holds
We already know: Q holds for an interval iff Q is true in the first state of that interval.
So (Q) means for each suffix interval σ′, Q is true in the first state of σ′.
Let σ ≜ σ0σ1σ2σ3 then σ satisfies (Q) iff for each suffix interval σ′ (of σ), Q is true in the first state of σ′.
σ′ = |
σ3 |
||||
● |
yes |
||||
Q |
|||||
σ′ = |
σ2 |
σ3 |
|||
● |
● |
yes |
|||
Q |
|||||
σ′ = |
σ1 |
σ2 |
σ3 |
||
● | ● | ● | yes |
||
Q | |||||
σ′ = |
σ0 |
σ1 |
σ2 |
σ3 |
|
● |
● |
● |
● |
yes |
|
Q |
|||||
σ = |
σ0 |
σ1 |
σ2 |
σ3 |
|
● |
● |
● |
● | ||
Q |
Q |
Q |
Q |
||
(diamond-i)
there exists a prefix interval for which f holds, f ≜ f ; true
The prefix intervals of σ are:
σ0 |
σ0σ1 |
σ0σ1σ2 |
(skip): there exists a prefix interval for which skip holds
We already know: skip holds for an interval iff the interval has two states.
So (skip) means there exists a prefix interval σ′ with exactly two states.
Let σ ≜ σ0σ1σ2 then σ satisfies (skip) iff there exists a prefix interval σ′ (of σ) with exactly two states.
σ′ = |
σ0 |
|||
● |
no | |||
σ′ = |
σ0 |
σ1 |
||
● |
● |
yes |
||
σ′ = | σ
0 | σ1 | σ2 |
|
● |
● |
● |
no | |
σ = |
σ0 |
σ1 |
σ2 |
|
● |
● |
● | ||
(box-i)
for each prefix interval f holds, f ≜¬¬f
The prefix intervals of σ are:
σ0 |
σ0σ1 |
σ0σ1σ2 |
σ0σ1σ2σ3 |
(Q): for each prefix interval Q holds
We already know: Q holds for an interval iff Q is true in the first state of that interval.
So (Q) means for each prefix interval σ′, Q is true in the first state of σ′.
Let σ ≜ σ0σ1σ2σ3 then σ satisfies (Q) iff for each prefix interval σ′ (of σ), Q is true in the first state of σ′.
σ′ = |
σ0 |
||||
● |
yes |
||||
Q |
|||||
σ′ = |
σ0 |
σ1 |
|||
● |
● |
yes |
|||
Q |
|||||
σ′ = |
σ0 |
σ1 |
σ2 |
||
● | ● | ● | yes |
||
Q | |||||
σ′ = |
σ0 |
σ1 |
σ2 |
σ3 |
|
● |
● |
● |
● |
yes |
|
Q |
|||||
σ = |
σ0 |
σ1 |
σ2 |
σ3 |
|
● |
● |
● |
● | ||
Q |
|||||
(diamond-a)
there exists a sub interval for which f holds, f ≜true ; f ; true
The sub intervals of σ are:
σ0 |
||
σ1 |
||
σ2 |
||
σ0 | σ1 | |
σ
1 |
σ2 |
|
σ0 |
σ1 |
σ2 |
(empty): there exists a sub interval for which empty holds
We already know: empty holds for an interval iff the interval has one state.
So (empty) means there exists a sub interval σ′ with exactly one state.
Let σ ≜ σ0σ1σ2 then σ satisfies (empty) iff there exists a sub interval σ′ (of σ) with exactly one state.
σ′ = |
σ0 |
|||
● |
yes |
|||
σ′ = |
σ1 |
|||
● |
yes |
|||
σ′ = |
σ2 |
|||
● |
yes |
|||
σ′ = | σ0 |
σ1 |
||
● | ● | no | ||
σ′ = | σ
1 |
σ2 |
||
● |
● |
no | ||
σ′ = |
σ0 |
σ1 |
σ2 |
|
● |
● |
● |
no | |
σ = |
σ0 |
σ1 |
σ2 |
|
● |
● |
● | ||
(box-a)
for each sub interval f holds, f ≜¬¬f
The sub intervals of σ are:
σ0 |
||
σ1 |
||
σ2 |
||
σ0 | σ1 | |
σ
1 |
σ2 |
|
σ0 |
σ1 |
σ2 |
(Q): for each sub interval Q holds
We already know: Q holds for an interval iff Q is true in the first state of that interval.
So (Q) means for each sub interval σ′, Q is true in the first state of σ′.
σ′ = | σ0 | |||
● |
yes |
|||
Q |
||||
σ′ = |
σ1 |
|||
● |
yes |
|||
Q |
||||
σ′ = |
σ2 |
|||
● |
yes |
|||
Q |
||||
σ′ = |
σ0 |
σ1 |
||
● |
● |
yes |
||
Q |
||||
σ′ = |
σ1 |
σ2 |
||
● |
● |
yes |
||
Q |
||||
σ′ = |
σ0 |
σ1 |
σ2 |
|
● |
● |
● |
yes |
|
Q |
||||
σ = |
σ0 |
σ1 |
σ2 |
|
● |
● |
● |
||
Q |
Q |
Q |
||
skipn, n ≥ 0
Length of an interval,
skip0 |
≜ | empty |
skipn |
≜ | skip ; skipn−1
,(n > 0) |
if f0 then f1 else f2
The traditional binary choice, if f0 then f1 else f2 ≜ (f0 ∧ f1) ∨ (¬f0 ∧ f2).
if f0 then f1
The traditional if then construct, if f0 then f1 ≜if f0 then f1 else true.
fin f
f holds in the final state, fin f ≜(empty ⊃ f).
skip2 ∧fin Q
skip2 : |
● |
● |
● |
skip2 ∧fin Q : | ● | ● | ● |
Q |
|||
Note: Q is allowed to hold in the first and second state.
halt f
Halt when f holds, halt f ≜(empty ≡ f).
skip2 ∧ halt Q
skip2 : |
● |
● |
● |
skip2 ∧halt Q : | ● | ● | ● |
¬Q | ¬Q | Q |
|
Note: Q is not allowed to hold in the first and second state.
keep f
For all sub intervals of two states f holds, keep f ≜(skip ⊃ f).
while f0 do f1
Traditional while loop, while f0 do f1 ≜ (f0 ∧ f1)∗∧fin ¬f0.
repeat f0 until f1
Traditional repeat loop, repeat f0 until f1 ≜ f0 ; (while ¬f1 do f0).