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 On Congruence Property of Scope Equivalence for Concurrent Programs with Higher\-Order Communication
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%A Masaki Murakami
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X Representation of scopes of names is important for analysis
and
verification of concurrent systems. However, it is
difficult to
represent the scopes of channel names precisely
with models based on
process algebra. We introduced a model
of concurrent systems with
higher\-order communication based
on graph rewriting in our previous
work. A bipartite
directed acyclic graph represents a concurrent
system that
consists of a number of processes and messages in
that
model. The model can represent the scopes of local
names precisely.
We defined an equivalence relation such
that two systems are
equivalent not only in their behavior
but in extrusion of scopes of
names. This paper shows that
the equivalence relation is a
congruence relation wrt
tau\-prefix, new\-name, replication and
composition even if
higher\-order communication is allowed. And we
also show
the equivalence relation is not congruent wrt
input\-prefix
though it is congruent wrt input prefix in
first\-order case.