A timed automaton A is a tuple (L, l₀, E, Label, C, clocks, guard, inv) [21] with

・ L, a non-empty, finite set of locations with initial location l₀ Є L

・ E ⊆ L x L, a set of edges

・ Label: L → 2^AP, a function that assigns to each location l Є L a set Label(l) of atomic propositions

・ C, a finite set of clocks

・ clocks: E → 2^C, a function that assigns to each edge e Є E a set of clocks clocks(e)

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.