On the operational semantics of timed rewrite systems

We propose an efficient operational semantics for a new class of rewrite systems, namely timed rewrite systems. This class constitute a conservative extension of first-order conditional term rewrite systems together with time features such as clocks, signals, timed terms, timed atoms and timed rules. We define first timed rewrite systems and illustrate them through some examples. A naive approach to the operational semantics is very costly in space. We propose, for a large class of programs, an improved calculus with a linear space complexity. Finally, we show how our framework compares to related work.