General Refinement, Part Two: Flexible Refinement

In the previous, companion, paper [13] to this paper we introduced our general model of refinement, discussed ideas around determinism and interfaces that the general definition raised, and gave several examples showing how the general definition could be specialised to the sorts of refinement we see in the literature. In this paper we continue the story and we define vertical refinement on our general model. Vertical refinement can be seen as a generalisation of what, in the literature, has been called action refinement or non-atomic refinement. Alternatively, by viewing a special model (from the previous paper) as a logical theory, vertical refinement can be seen as a theory morphism, formalised as a Galois connection. We give an example of the utility of this definition by constructing a vertical refinement between broadcast processes and interactive branching programs, and we see how interactive branching programs can be implemented on a platform which provides broadcast communica...

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Steve Reeves, David Streader
• Keywords: ENTCS 2008, General Definition, Paper, Vertical Refinement