Timed Automata

Timed Automata

Alexandre David

Aalborg University

Overview

Syntax & semantics Decidability results Regions

TCTL

Example: Dumb Light Control

WANT: if press is issued twice quickly

then the light will get brighter; otherwise the light is turned off.

Off ^press? Light ^press? Bright

press?

press?

Dumb Light Control

Off ^press? Light ^press? Bright

press?

press?

Solution: Add real-valued clock x

x:=0

x≤3

x>3

Alur & Dill 1990

Timed Automata

Off ^press? Light ^press? Bright

press?

press?

x:=0

x≤3

x>3

Alur & Dill 1990

Synchronizing action

Guard Conjunctions

of x~n x: real-

valued clock Reset

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

States:

( location , x=v) where v2R States:

( location , x=v) where v2R

Timed Automata

Off ^press? Light ^press? Bright

press?

press?

x:=0

x≤3

x>3

Alur & Dill 1990

Synchronizing action

Guard Conjunctions

of x~n x: real-

valued clock Reset

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

States:

( location , x=v) where v2R States:

( location , x=v) where v2R

Timed Automata

Off ^press? Light ^press? Bright

press?

press?

x:=0

x≤3

x>3

Alur & Dill 1990

Synchronizing action

Guard Conjunctions

of x~n x: real-

valued clock Reset

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

States:

( location , x=v) where v2R States:

( location , x=v) where v2R

Timed Automata

Off ^press? Light ^press? Bright

press?

press?

x:=0

x≤3

x>3

Alur & Dill 1990

Synchronizing action

Guard Conjunctions

of x~n x: real-

valued clock Reset

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

States:

( location , x=v) where v2R States:

( location , x=v) where v2R

Timed Automata

Off ^press? Light ^press? Bright

press?

press?

x:=0

x≤3

x>3

Alur & Dill 1990

Synchronizing action

Guard Conjunctions

of x~n x: real-

valued clock Reset

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 )

press? ( Bright , x=2.51 )

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 2.51 ( Light , x=2.51 ) press? ( Bright , x=2.51 ) States:

( location , x=v) where v2R States:

( location , x=v) where v2R

Intelligent Light Control

Off ^press? Light ^press? Bright

press?

x:=0

x≤3

x>3

Off ^press? Light ^press? Bright

press?

press?

X:=0

X<=3

X>3

x≤100 x=100

x:=0

x≤100 x=100

x:=0

x:=0

press?

x:=0

Using Invariants

x:=0

Intelligent Light Control

Off ^press? Light ^press? Bright

press?

x:=0

x≤3

x>3 x=100

x:=0

x=100 x:=0

x:=0

press?

x:=0

Using Invariants

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 4.51 ( Light , x=4.51 )

press? ( Light , x=0 )

delay 100 ( Light , x=100)

τ

Transitions:

( Off , x=0 )

delay 4.32 ( Off , x=4.32 )

press? ( Light , x=0 )

delay 4.51 ( Light , x=4.51 )

press? ( Light , x=0 )

delay 100 ( Light , x=100)

τ

Note:

( Light , x=0 ) delay 103 Note:

( Light , x=0 ) delay 103

X

Invariants ensures progress Invariants

ensures progress

x≤100 x:=0 x≤100

NTA: Light Controller & User

Off ^press? Light ^press? Bright

press?

x:=0

x≤3

x>3 x=100

x:=0

x=100 x:=0

x:=0

press?

x:=0

Rest Busy

y¸10

y:=0

y≤10 press!

press!

y:=0

Transitions:

( Off, Rest, x=0, y=0 )

delay 20 ( Off, Rest, x=20, y=20 ) press?! ( Light, Busy, x=0, y=0 ) delay 2 ( Light, Busy, x=2, y=2) press?! ( Bright, Rest, x=0, y=0) Transitions:

( Off, Rest, x=0, y=0 )

delay 20 ( Off, Rest, x=20, y=20 ) press?! ( Light, Busy, x=0, y=0 ) delay 2 ( Light, Busy, x=2, y=2) press?! ( Bright, Rest, x=0, y=0) Synchronization

x≤100 x:=0 x≤100

Timed Automata ^review

n

m a

Alur & Dill 1990

Clocks: x, y

x<=5 & y>3

x := 0

Guard

Boolean combination of integer bounds on clocks

Reset

Action performed 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

Discrete Trans

Delay Trans

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

Timed Automata ^review

Invariants

Invariants ensure progress!!

Invariants

ensure

progress!!

Syntax

A TA is a tuple (L,l ₀ ,E,I) where

L is a finite set of locations l ₀ ∈ L is the initial location

E ⊆ L × B(C) × Act × 2 ^C × L is a finite set of edges, and

I : L → B’(C) assigns invariants to locations.

C is a finite set of clocks.

B(C) is the set of clock constraints defined by g,g ₁ ,g ₂ :: = x ⊗ n | g ₁ ∧g ₂

⊗ ∈ { ≤,<,=,>,≥ }

Clock Valuations

For each d∈R _≥0 , the valuation v+d is defined by

(v + d)(x) = v(x) + d for each x ∈ C delay

For each r ⊆ C, the valuation v[r] is defined by

v[r](x) = 0 if x ∈r

v[r](x) = v(x) otherwise

reset

Semantics

The time transition system T(A) generated by A=(L,l ₀ ,E,I) is defined as

) ( and

) ( s.t.

all for )

, ( )

, (

) ' ( v' and ],

[ '

, s.t.

) ' (

if ) ' , ' ( )

, (

Act

I(l)}

and

) (

) , (

| ) , {(

Proc

) Lab

| Lab,

Proc, (

) (

0 ,

, 0

0

l I d v

l I v d

d v

l v

l

l I r

v v

g v

E l

l v

l v

l Lab

v C

L v

l v

l A

T

d

r a a g

+ ℜ

∈ +

→

=

∈

→

∃

→

ℜ

∪

=

ℜ

→

×

∈

=

⎭ ⎬

⎫

⎩ ⎨

⎧ → ∈

=

>=

>=

>=

α α

and time is continuous

TA in UPPAAL

Extended to NTA with syn. over channels.

+ urgency (urgent & committed locations, urgent channels)

+ variables

Symbolic semantics (see later).

) ], /

' , / ' [ ( )

, (

'

'

2 2

1 1

2

! 2 1

! 1

v l

l l l

l v

l

l l

l l

a a

→ α

→

→ (simplified, g,a,r missing)

Decidability?

Reachable?

a b

c

OBSTACLE:

Uncountable infinite

state space

Reachable States

TAB

States → Equivalence Classes

x y

An equivalence class (i.e. a region )

in fact there is only a finite number of regions!!

1 2 3

1 2

Regions

Finite Partitioning of State Space

Complexity

n=|C|

States ↔ Regions

x y

An equivalence class (i.e. a region )

Successor regions, Succ(r) r

1 2 3

1 2

Regions

Successor Operation (wrt delay)

x y

An equivalence class (i.e. a region ) r {x}r

{y}r r

Reset regions

1 2 3

1 2

Regions

Reset Operation

An Example Region Graph

Fundamental Results

Reachability ☺ ^{Alur, Dill} Trace-inclusion ^{Alur, Dill}

Timed ; Untimed ☺

Bisimulation

Timed ☺ Cerans ; Untimed ☺

Model-checking ☺

TCTL, T _mu , L _nu ,...

PS PA CE -c

PSP ACE -c / EXP TIME -c

Updatable Timed Automata

Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, Antoine Petit

W Diagonals

W Diagonals

TCTL = CTL + Time

−

−

∈

∈

φ α

in z

clocks formula

D z

ns propositio automic

AP p

, ,

, ,

“freeze operator” introduces new formula clock z

E[ φ U φ ], A[ φ U φ ] - like in CTL No EX φ

constraints over formula clocks and automata clocks

Derived Operators

Along any path φ holds continuously until within 7 time units ψ becomes valid.

=

=

The property φ becomes valid within 5 time units.

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)