Categorical modelling of trace equivalence for timed automata models with invariants

Formal models for real-time systems have been actively studied over the past several years. Much of the theory of untimed systems has been lifted to the real-time setting. An example is the notion of trace equivalence applied to timed transition systems with invariants which is studied here within the general categorical framework of open maps. In particular, we demonstrate how to characterize standard timed trace equivalence in terms of spans of open maps with a natural choice of a path category.