{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:25:31Z","timestamp":1740108331683,"version":"3.37.3"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3-5","license":[{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T00:00:00Z","timestamp":1588723200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000769","name":"University of Oxford","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000769","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hoare\u2019s Communicating Sequential Processes (CSP) (Hoare in Communicating Sequential Processes, Prentice-Hall Inc, Upper Saddle River, 1985) admits a rich universe of semantic models closely related to the van Glabbeek spectrum. In this paper we study finite observational models, of which at least six have been studied for CSP, namely traces, stable failures, revivals, acceptances, refusal testing and finite linear observations (Roscoe in Understanding concurrent systems. Texts in computer science, Springer, Berlin, 2010). (Others are known.) We show how to use the relatively recently-introduced <jats:italic>priority<\/jats:italic> operator (Roscoe in Understanding concurrent systems. Texts in Computer Science, Springer, Berlin, 2010) to transform refinement questions in these models into trace refinement (language inclusion) tests. Furthermore, we are able to generalise this to any (rational) finite observational model. As well as being of theoretical interest, this is of practical significance since the state-of-the-art refinement checking tool FDR4 (Gibson-Robinson et al. in Int J Softw Tools Technol Transf 18(2):149\u2013167, 2016) currently only supports two such models. In particular we study how it is possible to check refinement in a discrete version of the Timed Failures model that supports Timed CSP.<\/jats:p>","DOI":"10.1007\/s00236-020-00372-9","type":"journal-article","created":{"date-parts":[[2020,5,6]],"date-time":"2020-05-06T15:04:01Z","timestamp":1588777441000},"page":"403-438","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Translating between models of concurrency"],"prefix":"10.1007","volume":"57","author":[{"given":"David","family":"Mestel","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7557-3901","authenticated-orcid":false,"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,5,6]]},"reference":[{"key":"372_CR1","unstructured":"Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking Timed CSP. In: Proceedings of HOWARD (Festschrift for Howard Barringer) (2012)"},{"key":"372_CR2","doi-asserted-by":"crossref","unstructured":"Brinksma, E., Rensink, A., Vogler, W.: Fair testing. In: International Conference on Concurrency Theory, pp. 313\u2013327. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60218-6_23"},{"issue":"2","key":"372_CR3","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","volume":"138","author":"J Davies","year":"1995","unstructured":"Davies, J., Schneider, S.: A brief history of Timed CSP. Theor. Comput. Sci. 138(2), 243\u2013271 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"372_CR4","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3\u2014a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2014. Lecture Notes in Computer Science, vol. 8413, Springer, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"issue":"2","key":"372_CR5","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10009-015-0377-y","volume":"18","author":"T Gibson-Robinson","year":"2016","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149\u2013167 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"372_CR6","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical partial order reduction for CSP. In: Havelund K., Joshi R., Holzmann G. (eds.) NASA Formal Methods, pp. 188\u2013203. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-17524-9_14"},{"key":"372_CR7","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc, Upper Saddle River (1985)"},{"key":"372_CR8","unstructured":"Jackson, D.M.: Logical verification of reactive software systems. Oxford University, DPhil Thesis (1992)"},{"issue":"1","key":"372_CR9","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"issue":"1","key":"372_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. (STTT) 1(1), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"372_CR11","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/j.entcs.2016.09.041","volume":"325","author":"D Mestel","year":"2016","unstructured":"Mestel, D., Roscoe, A.W.: Reducing complex CSP models to traces via priority. Electron. Notes Theor. Comput. Sci. 325, 237\u2013252 (2016)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"372_CR12","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982)"},{"issue":"1","key":"372_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"372_CR14","unstructured":"Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. PhD thesis, Oxford University (2000)"},{"key":"372_CR15","doi-asserted-by":"crossref","unstructured":"Ouaknine, J.: Digitisation and full abstraction for dense-time model checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 37\u201351. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_4"},{"issue":"3","key":"372_CR16","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0304-3975(87)90117-4","volume":"50","author":"I Phillips","year":"1987","unstructured":"Phillips, I.: Refusal testing. Theor. Comput. Sci. 50(3), 241\u2013284 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"372_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0304-3975(98)00214-X","volume":"211","author":"GM Reed","year":"1999","unstructured":"Reed, G.M., Roscoe, A.W.: The timed failures\u2013stability model for CSP. Theor. Comput. Sci. 211(1\u20132), 85\u2013127 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"372_CR18","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"372_CR19","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: Seeing beyond divergence. In: Communicating Sequential Processes. The First 25 Years, pp. 15\u201335. Springer, Berlin (2005)","DOI":"10.1007\/11423348_2"},{"issue":"3","key":"372_CR20","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.jlap.2008.10.002","volume":"78","author":"AW Roscoe","year":"2009","unstructured":"Roscoe, A.W.: Revivals, stuckness and the hierarchy of CSP models. J. Logic Algebr. Program. 78(3), 163\u2013190 (2009)","journal-title":"J. Logic Algebr. Program."},{"key":"372_CR21","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, Berlin (2010)"},{"key":"372_CR22","unstructured":"Roscoe, A.W.: On the expressiveness of CSP (2011)"},{"key":"372_CR23","unstructured":"Roscoe, A.W.: The automated verification of timewise refinement. EIT- CPSE (2013)"},{"key":"372_CR24","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/j.entcs.2015.12.023","volume":"319","author":"AW Roscoe","year":"2015","unstructured":"Roscoe, A.W.: The expressiveness of CSP with priority. Electron. Notes Theor. Comput. Sci. 319, 387\u2013401 (2015)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"372_CR25","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0890-5401(87)90004-6","volume":"75","author":"AW Roscoe","year":"1987","unstructured":"Roscoe, A.W., Dathi, N.: The pursuit of deadlock freedom. Inf. Comput. 75(3), 289\u2013327 (1987)","journal-title":"Inf. Comput."},{"issue":"1","key":"372_CR26","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-012-0251-6","volume":"25","author":"AW Roscoe","year":"2013","unstructured":"Roscoe, A.W., Huang, J.: Checking noninterference in Timed CSP. Form. Asp. Comput. 25(1), 3\u201335 (2013)","journal-title":"Form. Asp. Comput."},{"key":"372_CR27","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"AW Roscoe","year":"1988","unstructured":"Roscoe, A.W., Reed, G.M.: A timed model for Communicating Sequential Processes. Theor. Comput. Sci. 58, 249\u2013261 (1988)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"372_CR28","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1995.1014","volume":"116","author":"S Schneider","year":"1995","unstructured":"Schneider, S.: An operational semantics for Timed CSP. Inf. Comput. 116(2), 193\u2013213 (1995)","journal-title":"Inf. Comput."},{"key":"372_CR29","volume-title":"Concurrent and Real-Time Systems","author":"S Schneider","year":"2000","unstructured":"Schneider, S.: Concurrent and Real-Time Systems. Wiley, Hoboken (2000)"},{"key":"372_CR30","volume-title":"A Second Course in Formal Languages and Automata Theory","author":"J Shallit","year":"2009","unstructured":"Shallit, J.: A Second Course in Formal Languages and Automata Theory. Cambridge University Press, Cambridge (2009)"},{"key":"372_CR31","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J.: The linear time-branching time spectrum II. In: International Conference on Concurrency Theory, pp. 66\u201381 (1993)","DOI":"10.1007\/3-540-57208-2_6"},{"key":"372_CR32","doi-asserted-by":"crossref","unstructured":"Van\u00a0Glabbeek, R.J.: The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In: Handbook of Process Algebra, pp. 3\u201399. Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"372_CR33","unstructured":"www.cs.ox.ac.uk\/people\/publications\/personal\/Bill.Roscoe.html (paper 193)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00372-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00372-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00372-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,5]],"date-time":"2021-05-05T23:27:16Z","timestamp":1620257236000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00372-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,6]]},"references-count":33,"journal-issue":{"issue":"3-5","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["372"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00372-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2020,5,6]]},"assertion":[{"value":"22 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 February 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}