Timed transition systems are a widely studied model for real-time systems. In this work we deal with an extension of this model, timed transition systems with invariants. The intention of the paper is to show applicability of the general categorical framework of open maps in order to treat the decidability question of the timed barbed bisimulation in the setting of the model being studied.
In particular, we define a category of timed transition systems with invariants, whose morphisms are to be considered as simulations of the behavior of one system by the other with an accuracy of τ-actions, and an accompanying (sub)category of path objects, for which the corresponding notions of open maps are developed. We then use the open maps framework to obtain the abstract bisimilarity and the path bisimilarity which are established to coincide with the timed barbed bisimulation. Finally, we consider the decidability question of the bisimulation studied in the setting of finite timed transition systems with invariants.