效绵县 Timed Automata extension of finite state machines with clocks continuous real semantics limited list of operations over clocks =automatic verification is feasible allowed operations: 0 comparison of a clock with a constant reset of a clock uniform flow of time (all clocks have the same rate)Timed Automata ◼ extension of finite state machines with clocks ◼ continuous real semantics ◼ limited list of operations over clocks  automatic verification is feasible ◼ allowed operations:  comparison of a clock with a constant  reset of a clock  uniform flow of time (all clocks have the same rate)