A timed automaton A is a tuple (L, l ・ L, a non-empty, finite set of locations with initial location l ・ E ⊆ L x L, a set of edges ・ Label: L → 2 ・ C, a finite set of clocks ・ clocks: E → 2 clocks: E → ψ (C), a function that assigns to each edge e Є E a set of clocks clocks(e) ・ guard: E → ψ (C),a function that labels each edge e Є E with a clock constraint guard(e) over C, and ・ inv: L → ψ (C), a function that assigns to each location an invariant. |