The decidability of reachability for pure public Mobile Ambients (i.e. without communication and restriction) has been recently investigated in [5], where a characterization of a maximal deacidable fragment is provided. A peculiar feature of such a fragment is the absence of the open capability for ambient dissolution. In this paper we analyse reachability in Boxed Ambients [2], the most relevant variant of Mobile Ambients in which the open capability is dropped and replaced by a sophisticated parent/child form of communication. The main novelties with respect to [5] are: (i) the definition of a more general notion of reachability (called target reachability); (ii) the proof of the decidability of target reachability for a richer calculus also comprising parent/child communication.
Reachability Analysis in Boxed Ambients / N. Busi; G. Zavattaro. - STAMPA. - 3701:(2005), pp. 143-159. (Intervento presentato al convegno 9th Italian Conference, ICTCS 2005 tenutosi a Siena, Italy nel October 12-14, 2005).
Reachability Analysis in Boxed Ambients
BUSI, NADIA;ZAVATTARO, GIANLUIGI
2005
Abstract
The decidability of reachability for pure public Mobile Ambients (i.e. without communication and restriction) has been recently investigated in [5], where a characterization of a maximal deacidable fragment is provided. A peculiar feature of such a fragment is the absence of the open capability for ambient dissolution. In this paper we analyse reachability in Boxed Ambients [2], the most relevant variant of Mobile Ambients in which the open capability is dropped and replaced by a sophisticated parent/child form of communication. The main novelties with respect to [5] are: (i) the definition of a more general notion of reachability (called target reachability); (ii) the proof of the decidability of target reachability for a richer calculus also comprising parent/child communication.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.