Previous Contents Next

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].


Previous Contents Next