Timed Automata, Timed Computation Tree Logic and CTL Models for Real Time Systems.

Slide1Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata and Timed Computation Tree Logic Paul Pettersson BRICS@Aalborg

Slide2Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. CTL Models = Kripke Structures

Slide3Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Computation Tree Logic, CTL Clarke & Emerson 1980 Syntax

Slide4Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. CTL, Derived Operators . . . . . . . . . . . . p p p AF p . . . . . . . . . . . . p EF p possible inevitable ”exists eventually” or ”reachable” ”exists globally”

Slide5Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. CTL, Derived Operators p p p . . . . . . . . . . . . AG p p p p p p p . . . . . . . . . . . . EG p p always potentially always for all paths next ”forall globally” or ”invariantly” ”forall eventually”

Slide6Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 18

Slide7Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide8Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide9Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide10Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide11Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide12Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide13Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide14Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Exercise 22

Slide15Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Off Light Bright press? Press? press? Press? WANT:   if press is issued twice  quickly then the  light  will get  brighter ; otherwise the light is turned  off. Timed Automata Intelligent Light Control

Slide16Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata Intelligent Light Control Off Light Bright Solution:  Add real-valued clock   x X:=0 X<=3 X>3 press? Press? press? Press?

Slide17Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata n m a (Alur & Dill 1990) Clocks :    x, y x<=5 & y>3 x := 0 Guard Boolean combination of comp with integer bounds Reset Action perfumed on clocks Transitions (   n  ,  x =2.4 ,  y =3.1415  )                                   (   n  ,  x =3.5 ,  y =4.2415  ) e(1.1) (   n  ,  x =2.4 ,  y =3.1415  )                                   (   m  ,  x =0 ,  y =3.1415  ) a State    (   location  ,  x =v ,  y =u  )     where v,u are in  R Action used for synchronization

Slide18Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. n m a Clocks:    x, y x<=5 & y>3 x := 0 Transitions (   n  ,  x =2.4 ,  y =3.1415  )                                   (   n  ,  x =3.5 ,  y =4.2415  )             e(1.1) (   n  ,  x =2.4 ,  y =3.1415  )         e(3.2) x<=5 y<=10 Location Invariants g1 g2 g3 g4  Invariants ensure progress!! Timed Safety Automata = Timed Automata + Invariants (Henzinger et al, 1992)

Slide19Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Clock Constraints

Slide20Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed (Safety) Automata

Slide21Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example guard reset location

Slide22Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example guard reset location

Slide23Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide24Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide25Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide26Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata: Example

Slide27Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Light Switch push push click

Slide28Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Light Switch • Switch may be turned on whenever at least 2 time units has elapsed since last “turn off” push push click

Slide29Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Light Switch • Switch may be turned on whenever at least 2 time units has elapsed since last “turn off” • Light automatically switches off after 9 time units. push push click

Slide30Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Semantics • clock valuations : • state : • Semantics of timed automata is a  labeled transition system where • action transition • delay Transition g  a  r l l’

Slide31Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Semantics: Example push push click

Slide32Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Networks of Timed Automata  + Integer Variables + arrays …. l1 l2 a! x>=2 i==3 x := 0 i:=i+4 m1 m2 a? y<=4       …………. Two-way synchronization on  complementary  actions. Closed Systems! ( l1 ,  m1 ,………, x=2, y=3.5, i=3,…..)              ( l2,m2 ,……..,x=0,  y=3.5, i=7,…..)  ( l1,m1 ,………,x=2.2, y=3.7, I=3,…..) 0.2 tau Example transitions If   a   URGENT CHANNEL

Slide33Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timed Automata in U PPAAL • Timed Safety Automata + urgent actions + urgent locations    (i.e. zero-delay locations) + committed locations    (i.e. zero-delay and  atomic  locations) + data-variables (integers with bounded domains) + arrays of data-variables + guards and assignments over data-variables and    arrays...

Slide34Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Urgent and Committed Locations m n o p q r 2.5 a committed urgent d d

Slide35Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. TCTL = CTL + Time constraints over formula clocks and automata clocks “freeze operator” introduces new formula clock z E[   U   ], A[   U    ]  - like in CTL No  EX  

Slide36Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Derived Operators Along any path   holds continuously until within 7 time units  becomes valid. = = The property   becomes valid within 5 time units.

Slide37Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Paths Example: push push click

Slide38Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Elapsed time in path Example:  

Slide39Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. TCTL Semantics s  - location w  - formula clock valuation P M ( s ) - set of paths from  s Pos (  ) - positions in    ,i) - elapsed time  (i,d) <<(i’,d’) iff (i<j) or ((i=j) and (d<d’))

Slide40Real-Time Systems, DTU, Feb 15, 2000Paul Pettersson, BRICS, Aalborg, Denmark. Timeliness Properties receive(m)  occurs within 5 time units after  send(m) receive(m)  occurs exactly 11 time units after  send(m) putbox  occurs periodically (exactly) every 25 time units (note: other  putbox ’s may occur in between)