Networks of Timed Automata
(..ni..nj.., ...xi=vi...xj=vj...)
(..mi...mj..., ...xi=0...xj=0...)
(..ni..nj.., ...xi=vi...xj=vj...)
(..ni..nj.., ...xi=vi+ri*d...xj=vj+rj*d...)
IF (v1,...,vk) satisfies gi and gj
IF ri is in [li,ui] and rj is in [lj,uj] and
(v1+r1*d,....,vn+rn*d) satisfies Inv(n1) ... Inv(nk)
and no synchronization on urgent actions becomes enabled.