ITL
© 1996-2018







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 finite 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 first 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 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 [Slide 54]

; (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.

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 definition: 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 definition, 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 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
  • (Q skip): n=0(Q skip)n

Sometimes [Slide 63]

(sometimes)

there exists a suffix interval for which f holds, f true ; f

Example 12.  

  • Let σ σ0σ1σ2 be an interval with 3 states.
  • 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 [Slide 67]

(always)

for each suffix interval f holds, f ¬¬f

Example 13.  

  • Let σ σ0σ1σ2σ3 be an interval with 4 states.
  • 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 [Slide 70]

(diamond-i)

there exists a prefix interval for which f holds, f f ; true

Example 14.  

  • Let σ σ0σ1σ2 be an interval with 3 states.
  • 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 [Slide 73]

(box-i)

for each prefix interval f holds, f ¬¬f

Example 15.  

  • Let σ σ0σ1σ2σ3 be an interval with 4 states.
  • 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 [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 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 [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 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 σ.

  • Let σ σ0σ1σ2 then σ satisfies (Q) iff for each sub interval σ (of σ), 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

Programming constructs [Slide 82]

skipn, n 0

Length of an interval,

skip0
empty
skipn
skip ; skipn1 , (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]

fin f

f holds in the final state, fin f (empty f).

Example 21.  

  • skip2 fin Q

    skip2 :
    skip2 fin Q :
    Q

    Note: Q is allowed to hold in the first 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 first 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) fin ¬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