Affiliations: A.P. Ershov Institute of Informatics Systems, SB RAS,
6, Acad. Lavrentiev av., Novosibirsk, 630090, Russia. [email protected] | A.P. Ershov Institute of Informatics Systems, SB RAS,
6, Acad. Lavrentiev av., Novosibirsk, 630090, Russia, and Novosibirsk State
University, 2, Pirogova st., Novosibirsk, 630090, Russia. [email protected]
Abstract: Timed transition systems are a widely studied model for real-time
systems. The intention of the paper is to show the applicability of the general
categorical framework of openmaps in order to prove that timed delay
equivalence is indeed an equivalence relation in the setting of timed
transition systems with invariants. In particular, we define a category of the
model under consideration and an accompanying (sub)category of observations to
which the corresponding notion of open maps is developed. We then use the open
maps framework to obtain an abstract equivalence relation which is established
to coincide with timed delay bisimulation.
