db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%T Efficient Simulation of CSP\-Like Languages
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%A Thomas Gibson\-Robinson
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%E Peter H. Welch, Frederick R. M. Barnes, Jan F. Broenink, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson
%B Communicating Process Architectures 2013
%X In \[dq]On the Expressiveness of CSP\[dq], 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 produced cannot be compiled by the CSP
model\-checker,
FDR. In this paper, we adapt Roscoe\[rs]s
simulation to make it produce a
process that can be checked
relatively efficiently by FDR. Further, we
extend
Roscoe\[rs]s simulation in order to allow recursively
defined
processes to be simulated 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.