Timed Automata

Timed Automata

Invariants

n

m

a

X:=0

X<=5 AND Yɯ

x<=5

y<=10

Location

invariants

(n, x = 2.4, y = 3.31)

e(3.2)

an invariant is a clock constraint

that specifies the amount of time that

may be spent in a location

(location) invariants are

used to force an edge to be taken

Diapositiva precedente

Diapositiva successiva

Torna alla prima diaposiva

Visualizza versione grafica