Action refinement for true concurrent real time

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper we develop action refinement technique in a real-time non-interleaving causality based setting, a timed extension of bundle event structures that allows for urgent interactions to model timeout. Syntactic action refinement operation is presented in a rimed process algebra based on the internationally standardised specification language LOTOS. We show that the behavior of the refined system can be inferred compositionally from the behavior of the original system and from the behaviors of the processes substituted for actions with explicitly represented start points, the rimed versions of a linear-time equivalence, pomset trace equivalence. and a branching-time equivalence, history preserving bisimulation equivalence, are both congruences under our refinement, and the syntactic and semantic action refinements we developed coincide under these equivalence notions with respect to a metric and a c.p.o. based denotational semantics. Therefore our refinement operations behave well. They meet the commonly expected properties.