A Propositional Branching Temporal Logic for the Ambient Calculus

We advocate the use of a CTL* logic, built upon the Ambient Calculus in dealing with mobile computing phenomena. Our logic is a more expressive alternative to Ambient Logic, based on a single modality, but still powerful enough to handle mobility and dynamic hierarchies of locations. In applications, the possibility of expressing path properties of computation together with state properties opens new perspectives. Moreover, having a temporal logic to express properties of computation, we can reuse the algorithms for model checking temporal logics in analyzing the phenomena described using Ambient Calculus. We resort to syntax trees of Ambient Calculus and enrich them with labelling functions that generates the state processes. These constitute a sound model for Ambient Calculus and are used as possible worlds in a Kripke structure developed for a propositional branching temporal logic. The accessibility relation is generated by the reduction of Ambient Calculus considered as reduction between syntax trees. We provide the algorithms able to compute, giving the initial state of a system, any possible next state. These algorithms could be used together with the algorithms for model checking temporal logic in order to develop model checking analysis for Ambient Calculus.