Modeling Urgency in Timed Systems

Timed systems can be modeled as automata (or, generally, discrete transition structures) extended with real-valued variables (clocks) measuring the time elapsed since their initialization. The following features are also common in the above models. States are associated with time progress conditions specifying how time can advance. Time can progress at a state by t only if all the intermediate states reached satisfy the associated time progress condition.At transitions, clock values can be tested and modified. This is usually done by associating with transitions guards (conditions on clocks) and assignments. If a guard is true from an automaton state and a given clock valuation, the corresponding transition can be executed by modifying clocks as specified by the corresponding assignment.