Timed automata extension of finite state machines with clocks continuous real semantics limited list of operations over clocks automatic verification is feasible allowed operations o comparison of a clock with a constant o reset of a clock o 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)
A What is a Timed Automaton? off o an automaton with locations(states) and edges the automaton spends time only in locations, not in eages
What is a Timed Automaton? ◼ an automaton with locations (states) and edges ◼ the automaton spends time only in locations, not in edges
A What is a Timed Automaton?(2) x>2 Z<3 off ) o r=9 real valued clocks(x, y, z) all clocks run at the same speed clock constraints can be guards on edges
What is a Timed Automaton? (2) ◼ real valued clocks (x, y, z) ◼ all clocks run at the same speed ◼ clock constraints can be guards on edges
o What is a Timed Automaton? (3)-i5 x>2x:=0 Z<3 off on y=0 x:=0,z:=0 clocks can be reset when taken an edge only a reset to value 0 is allowed
What is a Timed Automaton? (3) ◼ clocks can be reset when taken an edge ◼ only a reset to value 0 is allowed
A What is a Timed Automaton?(4) x>2x:=0 Z<5 z<3 off y 0.z:=0 location invariants forl bid to stay in a state too long invariants force taking an edge
What is a Timed Automaton? (4) ◼ location invariants forbid to stay in a state too long ◼ invariants force taking an edge