Syntax

2 Syntax

2.1 Input File

Our tool takes as an input an ASCII file containing the description of a closed mobile ambient. This description shall be recognized by the following grammar:

P	::=	(# n)P	(restriction)
		0	(inactivity)
		P \| ... \| P	(composition)
		n[P]	(ambient)
		cap	(capability action)
		io	(input/output action)


cap	::=	in n.P	(can enter n)
		out n.P	(can exit n)
		open n.P	(can open n)
		!open n.P	(can duplicate itself before opening n)
		á n ñ	(async output action)


io	::=	(n).P	(input action)
		!(n).P	(input action with duplication)
		á n ñ	(async output action)

Input action and restriction are the only name binders, in (n).P, !(n).P and (# n)P, occurrences n in P are bound. All other name occurrences are considered free.

2.2 Operational semantics

Name restriction introduces a fresh name in an agent; parallel composition allows in concurrently computing several agents in the same ambient; an agent can provide its surrounding ambient some capabilities: the capability to enter a col-located ambients, to exit from a surrounding ambient or the capability to dissolve a col-located ambient taking its content; agents can also communicate when located inside the same ambients, these communications are defined using substitution. We use a lazy version of replication: a resource is an agent which syntacticly duplicates itself before receiving a message. Lazy replications enable to trace agent creation. A formal definition of the operational semantics can be found in [6, Fig. 1].