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