Reducing Complex CSP Models to Traces via Priority

详细信息    查看全文

• 作者：David Mestel ^{david.mestel@cs.ox.ac.uk" class="auth_mail" title="E-mail the corresponding author} ; A.W. Roscoe ^{bill.roscoe@cs.ox.ac.uk" class="auth_mail" title="E-mail the corresponding author}
• 关键词：CSP ; denotational semantics ; priority
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2016
• 出版时间：5 October 2016
• 年：2016
• 卷：325
• 期：Complete
• 页码：237-252
• 全文大小：269 K

文摘

Hoare's Communicating Sequential Processes (CSP) [C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985] admits a rich universe of semantic models. In this paper we study finite observational models, of which at least six have been identified for CSP, namely traces, failures, revivals, acceptances, refusal testing and finite linear observations [A.W. Roscoe. Revivals, stuckness and the hierarchy of CSP models. The Journal of Logic and Algebraic Programming, 78(3):163–190, 2009]. We show how to use the recently-introduced priority operator ([A.W. Roscoe. Understanding Concurrent Systems. Texts in Computer Science. Springer, 2010], ch.20) 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 FDR3 [Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, and A.W. Roscoe. FDR3 – a modern refinement checker for CSP. In Tools and Algorithms for the Construction and Analysis of Systems, pages 187–201. Springer, 2014] currently only supports two such models.