Refining Emergent Properties

Systems which exhibit emergent behaviour, i.e., behaviour not determined by the behaviours of the constituents when considered in isolation, are becoming more common due to increasing use of distributed and decentralised designs. There have been claims that formal methods, and particularly refinement, can not be used to derive systems with emergent behaviour. In this paper, however, we argue that they can. To prove the point, we perform a refinement of an oft-cited example of emergence: the 'glider' pattern from Conway's Game of Life