Home | Search | Help  
Home Page Università di Genova

Technical Report Details


Date 14-10-2005
Number DISI-TR-05-16
Title Reachability Analysis of Mobile Ambients in Fragments of AC Term Rewriting
Authors Giorgio Delzanno, Roberto Montagna
Bibtex Entry
E-mail montagna@disi.unige.it
Link http://www.disi.unige.it/person/DelzannoG/Papers/dm06.pdf
Abstract In this paper we introduce a subclass of AC rewriting, called Tree Update Calculus (TUC), in which it is possible to specify update schemes for finite unordered trees with in which labels of nodes and leaves are taken from a finite set. The TUC reachability problem is undecidable. We isolate however a subclass of TUC, called structure preserving (TUCsp), in which reachability becomes decidable. In this fragment rules cannot shrink the tree structure of terms (thus open cannot be modelled). Despite of this restriction, TUCsp is still Turing equivalent. As an application, we will use TUCsp as a tool for reasoning in a uniform way on reachability problems for fragments of the Mobile Ambients of Cardelli and Gordon. More specifically, we will study the connections between TUCsp and open-free fragments of public MA with semantic and syntactic restrictions proposed in the literature. Decidability of reachability in these fragments follows from our result and from an encoding of their reduction semantics in TUCsp. Our result can also be applied to extensions of these MA fragments, e.g., with inter- and intra-ambient communication. Our analysis shows that a wide gamma of interesting programming abstractions could be added to MA without breaking the good properties of some of its dialects.
Back to Technical Reports