Timed Automata

With each switch one may associate a clock constraint, and

require that the switch may occur only if the current values of

the clocks satisfy this constraint.

With each location we associate a clock constraint called its

invariant,

and require that time can elapse in a location only as

long as its invariant stays true.

Timed Automata

S0

S1

x<=2

A, x:=0

x>=1, B

Diapositiva precedente

Diapositiva successiva

Torna alla prima diaposiva

Visualizza versione grafica