{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T00:31:09Z","timestamp":1695256269025},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2005,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            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\n            <jats:italic>P<\/jats:italic>\n            expressible as\n            <jats:italic>F<\/jats:italic>\n            (\n            <jats:italic>P<\/jats:italic>\n            )\u228f\n            <jats:italic>G<\/jats:italic>\n            (\n            <jats:italic>P<\/jats:italic>\n            ), where\n            <jats:italic>F<\/jats:italic>\n            and\n            <jats:italic>G<\/jats:italic>\n            are CSP contexts and \u228f 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\n            <jats:italic>F<\/jats:italic>\n            and\n            <jats:italic>G<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1007\/s00165-005-0065-x","type":"journal-article","created":{"date-parts":[[2005,6,28]],"date-time":"2005-06-28T09:21:11Z","timestamp":1119950471000},"page":"93-112","source":"Crossref","is-referenced-by-count":22,"title":["On the expressive power of CSP refinement"],"prefix":"10.1145","volume":"17","author":[{"given":"A.W.","family":"Roscoe","sequence":"first","affiliation":[{"name":"Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}]}],"member":"320","reference":[{"key":"p_1","unstructured":"[FDR] Formal Systems (Europe) Ltd. Failures-Divergence Refinement. User manual obtainable from http:\/\/www.formal.demon.co.uk\/fdr2manual\/index.html"},{"key":"p_2","volume-title":"Communicating sequential processes","author":"Hoa CAR","year":"1985"},{"key":"p_3","volume-title":"A semantic study of data-independence with applications to the mechanical verification of concurrent systems","author":"Laz RS","year":"1998"},{"key":"p_4","first-page":"99","volume-title":"LNCS 2021(DSSE-TR-2000-10)","author":"Leuschel A"},{"key":"p_5","volume-title":"A refusal testing model for CSP","author":"Muk A","year":"1993"},{"key":"p_6","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0304-3975(87)90117-4","article-title":"Refusal testing","volume":"50","author":"Phi I","year":"1987","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"p_7","first-page":"294","article-title":"Responsiveness of inter-operating components","volume":"16","author":"Reed JN","year":"2004","journal-title":"Form Aspects Comput"},{"key":"p_8","volume-title":"Reed, Roscoe, Wachter (eds) Topology and category theory in computer science","author":"Ros AW","year":"1991"},{"issue":"5","key":"p_9","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1093\/logcom\/2.5.557","article-title":"An alternative order for the failures model","volume":"2","author":"Ros AW","year":"1992","journal-title":"J Logic Comput"},{"key":"p_10","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1093\/logcom\/3.2.131","article-title":"Unbounded nondeterminism in CSP","volume":"3","author":"Ros AW","year":"1993","journal-title":"J Logic Comput"},{"key":"p_11","volume-title":"Proceedings of 1995 IEEE symposium on security and privacy IEEE Computer Society Press","author":"Ros AW","year":"1995"},{"key":"p_12","volume-title":"The theory and practice of concurrency","author":"Ros AW","year":"1998"},{"key":"p_14","volume-title":"Proceedings of CPA 2004 (IOS Press)","author":"Ros AW","year":"2004"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-005-0065-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-005-0065-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-005-0065-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:52:39Z","timestamp":1641484359000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-005-0065-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":13,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["10.1007\/s00165-005-0065-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-005-0065-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,8]]}}}