Timed Safety Automata = Timed Automata + Invariants

n

m

a

Clocks: x, y

x<=5 & yɯ

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᝺

Location

Invariants

g1

g2

g3

g4

(Henzinger et al, 1992)

Föregående bild

Nästa bild

Tillbaka till första bilden

Visa grafisk version