Previous Contents Next

3   Enforcing a link between agent and the channel names they declare

The 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 p-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 markers

The 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 neither the symbol 0 or e are elements of L. An agent marker is a word on the alphabet S=(L{0})2{Ext}.

3.2   Consistency

During a given computation sequence, the same marker can never be created twice.

This is still valid while only keeping the second component of each label pair in markers.

3.3   Name markers

Channel names are just stamped with the marker of the agent which has declared them. In the case where a name is declared by the context, it is given a marker in Ext*. 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.


Previous Contents Next