CONCUR 2004 – Concurrency Theory- P16: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 436 N. Markey and . Raskin - for each i either qi i qi or there exists a clock x . ui 1 rr Vi x r 4 - 4 . This ensures that at each step along that sequence either we change location or we reset at least one variable2. A position along a timed path t qi Vi Ii is a triple q v t eQx x R for which there exists an integer j . q q-j and v Vj t l Ij and t e Ij. For each i UiFj there exists exactly one position q v i along t which we denote by r t . Given a timed path t qi If and a position gj v t along p the suffix of p starting at position qj v t denoted by p- is the timed path where 1 q qi j for all i 2 vi j for i 0 and v o v 3 -t for i 0 and Zq i oo D Ij -t. Definition 2. A timed automaton TA is a 6-tuple A Q Qo H Z Inv T F where Q is a finite set of states Qo is a subset of Q containing the set of initial states H is a finite set of real-valued clocks I is a function Q 2AP labeling each state with atomic propositions of AP Inv is a function Q C H labeling each state with a set of timing constraints called invariants T C Q x C H x2H x Q is a set of transitions FQQ is a subset of Q containing the set of accepting states. In the sequel we generally identify a location q Q with its labeling l q if no ambiguity may arise from this notation. A position in a TA is a couple q v where q is a state and u is a valuation of clocks in H satisfying Inv g . Definition 3. Given a set of states Q and a set of clocks H a timed path i Vi Ii is a concretization of a TA Q Q0 H I Inv T if qo G Qo - For each j and for each t e Ij valuation Vj t l Ij satisfies Inv Qj - For each j there exists a transition qj p C qj f e E . valuation Vj r Ij l Ij satisfies and for all x C Vj i x 0 and for all x e H C Vj lW Vj x r Ij - l Ij . - either the timed path is infinite or its last state qn is accepting that is qn E F. Definition 4. Two clock valuations v and v are said to be equivalent . a family cx X H of constants if the following conditions hold - for all clocks x e H either both
