### 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]

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]

skipn, n 0

Length of an interval,

 skip0 ≜ empty skipn ≜ skip ; skipn−1 , (n > 0)

Example 18.

• skip3

 skip0 : ● skip1 : ● ● skip2 : ● ● ● skip3 : ● ● ● ●

#### Programming constructs [Slide 83]

if f0 then f1 else f2

The traditional binary choice, if f0 then f1 else f2 (f0 f1) (¬f0 f2).

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 f0 then f1

The traditional if then construct, if f0 then f1 if f0 then f1 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.

• skip2 ﬁn Q

 skip2 : ● ● ● skip2 ∧ﬁ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.

• skip2 halt Q

 skip2 : ● ● ● skip2 ∧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.

• skip2 keep Q

 skip2 : ● ● ● skip2 ∧keep Q : ● ● ● Q Q

#### Programming constructs [Slide 88]

while f0 do f1

Traditional while loop, while f0 do f1 (f0 f1) ﬁn ¬f0.

Example 24.

• skip2 while Q do skip

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

#### Programming constructs [Slide 89]

repeat f0 until f1

Traditional repeat loop, repeat f0 until f1 f0 ; (while ¬f1 do f0).

Example 25.

• skip2 repeat skip until Q

 skip2 : ● ● ● skip2 ∧repeat skip until Q : ● ● ● ¬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.

 2018-03-10 Contact | Home | ITL home | Course | Proofs | Algebra | FL