On the expressive power of CSP refinement |
| |
Authors: | A.W. Roscoe |
| |
Affiliation: | (1) Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK |
| |
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.Received November 2003Revised July 2004Accepted December 2004 by M. Leuschel and D. J. Cooke |
| |
Keywords: | CSP Refinement Topology Full abstraction |
本文献已被 SpringerLink 等数据库收录! |
|