效绵县 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)
效绵鼎 What is a Timed Automaton? off on an automaton with locations (states)and edges the automaton spends time only in locations,not in edges
What is a Timed Automaton? ◼ an automaton with locations (states) and edges ◼ the automaton spends time only in locations, not in edges
效绵县 What is a Timed Automaton?(2) X>2 Z<3 off on y=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
效绵鼎 What is a Timed Automaton?(3) x>2X:=0 z<3 off on y:=0 y=9 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
效绵鼎 What is a Timed Automaton?(4) X>2 x:=0 z<5 z<3 X<3 off on y:=C 9 X:=0,Z:=0 ■ location invariants forbid 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