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"
@InProceedings{GibsonRobinson13a,
title = "{E}fficient {S}imulation of {CSP}-{L}ike {L}anguages",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
author= "Gibson-Robinson, Thomas",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
editor= "Welch, Peter H. and Barnes, Frederick R. M. and Broenink, Jan F. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
pages = "185--204",
booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2013",
isbn= "978-0-9565409-7-3",
year= "2013",
month= "nov",
abstract= "In \textquotedblOn the Expressiveness of CSP\textquotedbl,
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's
simulation to make it produce a
process that can be checked
relatively efficiently by FDR. Further, we
extend Roscoe'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."
}