效绵鼎 Clock Constraints Definition:Let X be a set of clock variables.Then set C)of clock constraints is given by the following grammar: 0=X≤k|k≤x|x<k|k<x|0A0 where x∈X,k∈N
Clock Constraints ◼
效绵鼎 Timed Automata Syntax Definition:A timed automaton is a 4-tuple: A=(L,X,Io.E) o L is a finite set of locations o Xis a finite set of clocks o1oEL is an initial location oE∈L×C(X)×2x×L is a set of edges ■ 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: 0 waiting-only clock valuation changes 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+ v[Y :=0 is the valuation obtained fromv by resetting clocks from Y: vIr =01)- x∈Y otherwise v+d=flow of time (d units): (v+d)(x)=v(x)+d v=c means that valuation v satisfies the constraint c (a natural semantics)
Clock Valuations ◼
效绵县 Evaluation of Clock Constraints Evaluation of a clock constraint (vEg): vFx<k iffv(x)<k ■v乍x≤k iff v(x)≤k vFgAg2iffvF g1 andvFg2
Evaluation of Clock Constraints ◼