Efficient Simulation of CSP−Like Languages
Thomas Gibson−Robinson · Communicating Process Architectures · 2013
In On the Expressiveness of CSP, Roscoe provides a construction that, given the operational semantics rules of a CSP-like language and a process in that language, constructs a strongly bisimilar CSP process. Unfortunately, the construction provided is difficult to use and the scripts that it produces cannot be compiled by the CSP model-checker, FDR. In this paper we adapt Roscoe's simulation in order to make it produce a process that can be checked relatively efficiently by FDR. Further, we ex- tend Roscoe's simulation in order to allow recursively defined processes to be simu- lated in FDR, which was not supported by the original simulation. We also describe the construction of a tool that can automatically construct the simulation, given the operational semantics of the language and a script to simulate, both in an easy-to-use format.