On the expressive power of CSP refinement
Andrew William Roscoe · Formal Aspects of Computing · 2005
Abstract We show that wide-ranging classes of predicates on the failures-divergences model for CSP can be represented by refinement checks in a general form. These are predicates of a process P expressible as F ( P )⊏ G ( P ), where F and G are CSP contexts and ⊏ is refinement. We use ideas similar to full abstraction, but achieve a stronger property than that. Our main result is that topologically-closed predicates are precisely those representable when F and G are both uniformly continuous. We show that sub-classes of predicates such as refinement-closed and distributive ones are represented by special forms of this check.