Clock Constraints Definition: Let X be a set of clock variables. Then set C(X) of clock constraints is given by the following grammar 0=x≤k|k≤x|x<k|k<x|0∧0 where x∈X,k∈N
Clock Constraints ◼
Timed Automata syntax Definition:a timed automaton is a 4-tuple A=L,X,lo, E) o is a finite set of locations o X is a finite set of clocks nOel is an initial location oEsL×C(X)×2x× L is a set of edges a edge=(source location, clock constraint, set of clocks to be reset, target location)
Timed Automata Syntax ◼
Semantics: Main Idea semantics is a state space(reminder: guarded command language, extended finite state machines) states given by o location (local state of the automaton) o clock valuation ■ transitions o waiting--only clock valuation changes o action-change of location
Semantics: Main Idea ◼ semantics is a state space (reminder: guarded command language, extended finite state machines) ◼ states given by: location (local state of the automaton) clock valuation ◼ transitions: waiting — only clock valuation changes action — change of location
Clock valuations ■ a clock valuation is a function v:X→R vIY: =0] is the valuation obtained from by resetting clocks from Y [Y≥=0](x)= 0 x∈Y x otherwise v+d= flow of time(d units) (v+a)(x)=1(x)+d v Fc means that valuation v satisfies the constraint c(a natural semantics)
Clock Valuations ◼
Evaluation of Clock Constraints Evaluation of a clock constraint (v F g) v卡x<kiu(x)<k vx≤kifu(x)≤k VFg,g2 iff v F g1 and v i g2
Evaluation of Clock Constraints ◼