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]

more

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)^{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

(Q∧skip)^{∗}: ∨_{n=0}(Q∧skip)^{n}

Sometimes [Slide 63]

(sometimes)

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

Example 12.

Let σ≜σ_{0}σ_{1}σ_{2} be an interval with 3 states.

The suﬃx intervals of σ are:

σ_{2}

σ_{1}σ_{2}

σ_{0}σ_{1}σ_{2}

(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 σ≜σ_{0}σ_{1}σ_{2} then σ satisﬁes(Q) iﬀ there exists a suﬃx interval
σ′ (of σ) such that Q is true in the ﬁrst 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 [Slide 67]

(always)

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

Example 13.

Let σ≜σ_{0}σ_{1}σ_{2}σ_{3} be an interval with 4 states.

The suﬃx intervals of σ are:

σ_{3}

σ_{2}σ_{3}

σ_{1}σ_{2}σ_{3}

σ_{0}σ_{1}σ_{2}σ_{3}

(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 σ≜σ_{0}σ_{1}σ_{2}σ_{3} then σ satisﬁes(Q) iﬀ for each suﬃx interval
σ′ (of σ), Q is true in the ﬁrst 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 [Slide 70]

(diamond-i)

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

Example 14.

Let σ≜σ_{0}σ_{1}σ_{2} be an interval with 3 states.

The preﬁx intervals of σ are:

σ_{0}

σ_{0}σ_{1}

σ_{0}σ_{1}σ_{2}

(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 σ≜σ_{0}σ_{1}σ_{2} then σ satisﬁes(skip) iﬀ there exists a preﬁx
interval σ′ (of σ) with exactly two states.

σ′ =

σ_{0}

●

no

σ′ =

σ_{0}

σ_{1}

●

●

yes

σ′ =

σ_{
0}

σ_{1}

σ_{2}

●

●

●

no

σ =

σ_{0}

σ_{1}

σ_{2}

●

●

●

Box-i [Slide 73]

(box-i)

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

Example 15.

Let σ≜σ_{0}σ_{1}σ_{2}σ_{3} be an interval with 4 states.

The preﬁx intervals of σ are:

σ_{0}

σ_{0}σ_{1}

σ_{0}σ_{1}σ_{2}

σ_{0}σ_{1}σ_{2}σ_{3}

(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 σ≜σ_{0}σ_{1}σ_{2}σ_{3} then σ satisﬁes(Q) iﬀ for each preﬁx interval
σ′ (of σ), Q is true in the ﬁrst 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 [Slide 76]

(diamond-a)

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

Example 16.

Let σ≜σ_{0}σ_{1}σ_{2} be an interval with 3 states.

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 iﬀ the interval has
one state. So (empty) means there exists a sub interval σ′ with
exactly one state.

Let σ≜σ_{0}σ_{1}σ_{2} then σ satisﬁes(empty) iﬀ 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 [Slide 79]

(box-a)

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

Example 17.

Let σ≜σ_{0}σ_{1}σ_{2} be an interval with 3 states.

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 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 σ≜σ_{0}σ_{1}σ_{2} then σ satisﬁes(Q) iﬀ for each sub interval σ′
(of σ), Q is true in the ﬁrst 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

Programming constructs [Slide 82]

skip^{n}, n ≥ 0

Length of an interval,

skip^{0}

≜

empty

skip^{n}

≜

skip;skip^{n−1
}, (n > 0)

Example 18.

skip^{3}

skip^{0}:

●

skip^{1}:

●

●

skip^{2}:

●

●

●

skip^{3}:

●

●

●

●

Programming constructs [Slide 83]

iff_{0}thenf_{1}elsef_{2}

The traditional binary choice, iff_{0}thenf_{1}elsef_{2}≜(f_{0}∧f_{1})∨(¬f_{0}∧f_{2}).

Example 19.

ifAthen(¬B∧skip)else(B∧skip)

A∧¬B∧skip:

●

●

A,¬B

¬A∧B∧skip:

●

●

¬A,B

Programming constructs [Slide 84]

iff_{0}thenf_{1}

The traditional ifthen construct, iff_{0}thenf_{1}≜iff_{0}thenf_{1}elsetrue.

Example 20.

ifAthen(¬B∧skip)

A∧¬B∧skip:

●

●

A,¬B

¬A∧true:

●

…

¬A

Programming constructs [Slide 85]

ﬁnf

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

Example 21.

skip^{2}∧ﬁnQ

skip^{2}:

●

●

●

skip^{2}∧ﬁnQ :

●

●

●

Q

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

Programming constructs [Slide 86]

haltf

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

Example 22.

skip^{2}∧haltQ

skip^{2}:

●

●

●

skip^{2}∧haltQ :

●

●

●

¬Q

¬Q

Q

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

Programming constructs [Slide 87]

keepf

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

Example 23.

skip^{2}∧keepQ

skip^{2}:

●

●

●

skip^{2}∧keepQ :

●

●

●

Q

Q

Programming constructs [Slide 88]

whilef_{0}dof_{1}

Traditional while loop, whilef_{0}dof_{1}≜(f_{0}∧f_{1})^{∗}∧ﬁn¬f_{0}.

Example 24.

skip^{2}∧whileQdoskip

skip^{2}:

●

●

●

skip^{2}∧whileQdoskip:

●

●

●

Q

Q

¬Q

Programming constructs [Slide 89]

repeatf_{0}untilf_{1}

Traditional repeat loop, repeatf_{0}untilf_{1}≜f_{0};(while¬f_{1}dof_{0}).

Example 25.

skip^{2}∧repeatskipuntilQ

skip^{2}:

●

●

●

skip^{2}∧repeatskipuntilQ :

●

●

●

¬Q

Q

State and static variables [Slide 90]

State variables

State variables can possibly change within an interval and are denoted by
an initial capital symbol.

Static variables

Static variables remain constant within an interval and are denoted by
non-capital symbols.