3 Enforcing a link between agent and the channel names they declareThe link between agents and the names they have declared is usually lost by a-conversion. We propose to restore this link by enriching the syntax of
the ambient-calculus with markers. An unambiguous marker is inferred to
each instance of agent and then, each channel name is stamped with the
marker of its creating instance. This way a name is entirely identified
by the restriction operator which has declared it and its marker.
3.1 Agent markersThe marker of an agent is the history of the replications which had
led to its creation.
We first locate each action of the system by using a finite set of
labels L. We assume that the symbol e are elements of L.
An agent marker is a word on the alphabet S=L2.
Initial thread markers are the empty word;
- when computing agents, markers are always passed to agents
in the continuation;
- when fetching a resource, spawned agents are allocated a new
marker which is given by (i,j).id where i is the label of the
is the label of the agent which duplicate the resource and id is the marker of the duplicator agent,
During a given computation sequence, the same marker can never be
This is still valid while only keeping the second component of each label pair in markers.
3.3 Name markersNames are just stamped with the marker of the agent which has
Because of marker consistency, if two names are stamped
with the same agent marker, they have been declared by the same
instance of an agent.