More Relational Concurrent Refinement: Traces and Partial Relations

AbstractData refinement in a state-based language such as Z is defined using a relational model in terms of the behaviour of abstract programs. Downward and upward simulation conditions form a sound and jointly complete methodology to verify relational data refinements. On the other hand, refinement in a process algebra takes a number of different forms depending on the exact notion of observation chosen, which can include the events a system is prepared to accept or refuse.In this paper we continue our program of deriving relational simulation conditions for process algebraic refinement by defining further embeddings into our relational model: traces, completed traces, failure traces and extension