Introduction

III.1 Introduction

System behaviour [Slide 49]

We need a logic to rigorously describe the behaviour of systems. What is a behaviour?

Example 7.

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

System behaviour [Slide 50]

A Snapshot of system contains the variables of the system plus the values of those variables.
A Behaviour of the system is a sequence of snapshots of the system.
Convention: we will consider only ﬁnite sequences and only sequences with at least 1 snapshot (state).

System behaviour [Slide 51]

How to formally describe/specify a behaviour of a system?

Propositional logic is not adequate as it can only describe single snapshots of the system.
One needs temporal operators to describe/specify sequences (intervals) of system snapshots
Propositional Interval Temporal Logic can describe sequences of system snapshots using temporal operators

Skip [Slide 52]

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 ﬁrst state Q holds

●

●
Q

Propositional Formula [Slide 53]

What if you only got Q as formula?

Q: any interval of states such that in the ﬁrst 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 (ﬁnite and contains at least 1 state). The length of the interval is unconstrained and the states within the interval are also unconstrained.

●
…

Chop [Slide 54]

; (chop)

concatenate (fuse) two intervals together such that the last state of the ﬁrst interval is the same as ﬁrst state of the second interval.

Example 8.

skip ; skip

skip :	●	●
skip :		●	●

skip ; skip :	●	●	●

Next [Slide 55]

(Next)

f holds from the next state onwards, f ≜skip ; f.

Example 9.

(Q ∧skip) using the deﬁnition: skip ; (Q ∧skip)

skip :	●	●

Q ∧skip :		●	●
		Q

skip ; (Q ∧skip) :	●	●	●
		Q

More and Empty [Slide 56]

interval with at least two states, more ≜ true.

more :
●
●
…

empty

interval with only one state, empty ≜ ¬more.

empty :
●

Weak Next [Slide 57]

(Weak Next)

either an interval of only one state or f holds from the next state onwards, f ≜empty ∨ f.

Example 10.

(Q ∧ skip) is equal to, using the deﬁnition, empty ∨ (Q ∧ skip) and thus to

empty :
●

(Q ∧skip) :

●

●

●

Q

Chopstar [Slide 58]

^∗ (chopstar)

Finite number of fusion of intervals.

Example 11.

(Q ∧skip)^∗:

Fuse a ﬁnite number of times an interval satisfying (Q ∧skip).
Interval satisfying Q ∧skip:

Q ∧skip :
●
●

Q

0 times fusion:

Q ∧skip :
●
●

Q

(Q ∧skip)⁰ :

●

Interval contains only 1 unconstrained state.

1 time fusion:

Q ∧skip :
●
●

Q

(Q ∧skip)¹ :

●

●

Q

2 times fusion:

Q ∧skip :
●
●

Q

Q ∧skip :

●

●

Q

(Q ∧skip)² :

●

●

●

Q

Q

n times fusion:

(Q ∧skip)ⁿ :
●
●
…
●
●

Q

Q

…

Q
(Q ∧skip)^∗: ∨ _n=0(Q ∧skip)ⁿ

Sometimes [Slide 63]

(sometimes)

there exists a suﬃx interval for which f holds, f ≜true ; f

Example 12.

Let σ ≜ σ₀σ₁σ₂ be an interval with 3 states.
The suﬃx intervals of σ are:

σ₂

σ₁σ₂

σ₀σ₁σ₂

(Q): there exists a suﬃx interval for which Q holds

We already know: Q holds for an interval iﬀ Q is true in the ﬁrst state of that interval.

So (Q) means there exists a suﬃx interval σ′ such that Q is true in the ﬁrst state of σ′.

Let σ ≜ σ₀σ₁σ₂ then σ satisﬁes (Q) iﬀ there exists a suﬃx interval σ′ (of σ) such that Q is true in the ﬁrst state of σ′.

σ′ =			σ₂
			●	no
			¬Q
σ′ =		σ₁	σ₂
		●	●	yes
		Q
σ′ =	σ₀	σ₁	σ₂
	●	●	●	no
	¬Q

σ =	σ₀	σ₁	σ₂
	●	●	●
	¬Q	Q	¬Q

Are there any other intervals σ ≜ σ₀σ₁σ₂ that satisfy (Q)?

Always [Slide 67]

(always)

for each suﬃx interval f holds, f ≜¬¬f

Example 13.

Let σ ≜ σ₀σ₁σ₂σ₃ be an interval with 4 states.
The suﬃx intervals of σ are:

σ₃

σ₂σ₃

σ₁σ₂σ₃

σ₀σ₁σ₂σ₃

(Q): for each suﬃx interval Q holds

We already know: Q holds for an interval iﬀ Q is true in the ﬁrst state of that interval.

So (Q) means for each suﬃx interval σ′, Q is true in the ﬁrst state of σ′.

Let σ ≜ σ₀σ₁σ₂σ₃ then σ satisﬁes (Q) iﬀ for each suﬃx interval σ′ (of σ), Q is true in the ﬁrst state of σ′.

σ′ =				σ₃
				●	yes
				Q
σ′ =			σ₂	σ₃
			●	●	yes
			Q
σ′ =		σ₁	σ₂	σ₃
		●	●	●	yes
		Q
σ′ =	σ₀	σ₁	σ₂	σ₃
	●	●	●	●	yes
	Q

σ =	σ₀	σ₁	σ₂	σ₃
	●	●	●	●
	Q	Q	Q	Q

Diamond-i [Slide 70]

(diamond-i)

there exists a preﬁx interval for which f holds, f ≜ f ; true

Example 14.

Let σ ≜ σ₀σ₁σ₂ be an interval with 3 states.
The preﬁx intervals of σ are:

σ₀

σ₀σ₁

σ₀σ₁σ₂

(skip): there exists a preﬁx interval for which skip holds

We already know: skip holds for an interval iﬀ the interval has two states.

So (skip) means there exists a preﬁx interval σ′ with exactly two states.

Let σ ≜ σ₀σ₁σ₂ then σ satisﬁes (skip) iﬀ there exists a preﬁx interval σ′ (of σ) with exactly two states.

σ′ =	σ₀
	●			no

σ′ =	σ₀	σ₁
	●	●		yes

σ′ =	σ₀	σ₁	σ₂
	●	●	●	no


σ =	σ₀	σ₁	σ₂
	●	●	●

Box-i [Slide 73]

(box-i)

for each preﬁx interval f holds, f ≜¬¬f

Example 15.

Let σ ≜ σ₀σ₁σ₂σ₃ be an interval with 4 states.
The preﬁx intervals of σ are:

σ₀

σ₀σ₁

σ₀σ₁σ₂

σ₀σ₁σ₂σ₃

(Q): for each preﬁx interval Q holds

We already know: Q holds for an interval iﬀ Q is true in the ﬁrst state of that interval.

So (Q) means for each preﬁx interval σ′, Q is true in the ﬁrst state of σ′.

Let σ ≜ σ₀σ₁σ₂σ₃ then σ satisﬁes (Q) iﬀ for each preﬁx interval σ′ (of σ), Q is true in the ﬁrst state of σ′.

σ′ =	σ₀
	●				yes
	Q
σ′ =	σ₀	σ₁
	●	●			yes
	Q
σ′ =	σ₀	σ₁	σ₂
	●	●	●		yes
	Q
σ′ =	σ₀	σ₁	σ₂	σ₃
	●	●	●	●	yes
	Q

σ =	σ₀	σ₁	σ₂	σ₃
	●	●	●	●
	Q

Diamond-a [Slide 76]

(diamond-a)

there exists a sub interval for which f holds, f ≜true ; f ; true

Example 16.

Let σ ≜ σ₀σ₁σ₂ be an interval with 3 states.
The sub intervals of σ are:

σ₀

σ₁

σ₂

σ₀
σ₁

σ₁

σ₂

σ₀

σ₁

σ₂

(empty): there exists a sub interval for which empty holds

We already know: empty holds for an interval iﬀ the interval has one state.

So (empty) means there exists a sub interval σ′ with exactly one state.

Let σ ≜ σ₀σ₁σ₂ then σ satisﬁes (empty) iﬀ there exists a sub interval σ′ (of σ) with exactly one state.

σ′ =	σ₀
	●			yes
σ′ =		σ₁
		●		yes
σ′ =			σ₂
			●	yes
σ′ =	σ₀	σ₁
	●	●		no
σ′ =		σ₁	σ₂
		●	●	no
σ′ =	σ₀	σ₁	σ₂
	●	●	●	no

σ =	σ₀	σ₁	σ₂
	●	●	●

Box-a [Slide 79]

(box-a)

for each sub interval f holds, f ≜¬¬f

Example 17.

Let σ ≜ σ₀σ₁σ₂ be an interval with 3 states.
The sub intervals of σ are:

σ₀

σ₁

σ₂

σ₀
σ₁

σ₁

σ₂

σ₀

σ₁

σ₂

(Q): for each sub interval Q holds

We already know: Q holds for an interval iﬀ Q is true in the ﬁrst state of that interval.

So (Q) means for each sub interval σ′, Q is true in the ﬁrst state of σ′.
Let σ ≜ σ₀σ₁σ₂ then σ satisﬁes (Q) iﬀ for each sub interval σ′ (of σ), Q is true in the ﬁrst state of σ′.

σ′ =	σ₀
	●			yes
	Q
σ′ =		σ₁
		●		yes
		Q
σ′ =			σ₂
			●	yes
			Q
σ′ =	σ₀	σ₁
	●	●		yes
	Q
σ′ =		σ₁	σ₂
		●	●	yes
		Q
σ′ =	σ₀	σ₁	σ₂
	●	●	●	yes
	Q

σ =	σ₀	σ₁	σ₂
	●	●	●
	Q	Q	Q

Programming constructs [Slide 82]

skipⁿ, n ≥ 0

Length of an interval,

skip⁰	≜	empty
skipⁿ	≜	skip ; skipⁿ⁻¹,(n > 0)

Example 18.

skip³

skip⁰ :

●

skip¹ :

●

●

skip² :
●
●
●

skip³ :

●

●

●

●

Programming constructs [Slide 83]

if f₀ then f₁ else f₂

The traditional binary choice, if f₀ then f₁ else f₂ ≜ (f₀ ∧ f₁) ∨ (¬f₀ ∧ f₂).

Example 19.

if A then (¬B ∧skip) else (B ∧skip)

A ∧¬B ∧skip :	●	●
	A,¬B
¬A ∧ B ∧skip :	●	●
	¬A,B

Programming constructs [Slide 84]

if f₀ then f₁

The traditional if then construct, if f₀ then f₁ ≜if f₀ then f₁ else true.

Example 20.

if A then (¬B ∧skip)

A ∧¬B ∧skip :	●	●
	A,¬B
¬A ∧true :	●	…
	¬A

Programming constructs [Slide 85]

ﬁn f

f holds in the ﬁnal state, ﬁn f ≜(empty ⊃ f).

Example 21.

skip² ∧ﬁn Q

skip² :

●

●

●

skip² ∧ﬁn Q :
●
●
●

Q

Note: Q is allowed to hold in the ﬁrst and second state.

Programming constructs [Slide 86]

halt f

Halt when f holds, halt f ≜(empty ≡ f).

Example 22.

skip² ∧ halt Q

skip² :

●

●

●

skip² ∧halt Q :
●
●
●

¬Q
¬Q
Q

Note: Q is not allowed to hold in the ﬁrst and second state.

Programming constructs [Slide 87]

keep f

For all sub intervals of two states f holds, keep f ≜(skip ⊃ f).

Example 23.

skip² ∧keep Q

skip² :

●

●

●

skip² ∧keep Q :
●
●
●

Q
Q

Programming constructs [Slide 88]

while f₀ do f₁

Traditional while loop, while f₀ do f₁ ≜ (f₀ ∧ f₁)^∗∧ﬁn ¬f₀.

Example 24.

skip² ∧while Q do skip

skip² :	●	●	●
skip² ∧while Q do skip :	●	●	●
	Q	Q	¬Q

Programming constructs [Slide 89]

repeat f₀ until f₁

Traditional repeat loop, repeat f₀ until f₁ ≜ f₀ ; (while ¬f₁ do f₀).

Example 25.

skip² ∧ repeat skipuntil Q

skip² :	●	●	●
skip² ∧repeat skipuntil Q :	●	●	●
		¬Q	Q

2023-09-12

Q ∧skip :	●	●
	Q
Q ∧skip :		●	●
		Q

(Q ∧skip)² :	●	●	●
	Q	Q

skip⁰ :	●
skip¹ :	●	●
skip² :	●	●	●
skip³ :	●	●	●	●