Reachability Analysis in Boxed Ambients

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.