Operational semantics for real-time processes with action refinement

In this paper we propose an event-based operational interleaving semantics for a real-time process algebra, for which action refinement and a denotational true concurrency semantics have been developed and defined in terms of timed event structures. We characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics.