Relational Concurrent Refinement: Automata

Data 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. In models of concurrency, refinement 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, or depend on explicit properties of states and transitions.

In this paper we continue our program of deriving relational simulation conditions for behavioural notions of refinement by defining embeddings into the relational model that extend our framework to include various notions of automata based refinement.