An Analysis for Causal Properties of Membrane Interactions

We present here an analysis, based on Abstract Interpretation [P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages (POPLʼ77), pp. 238–252, 1977.], obtained by defining a finite computable approximation of the causal semantics proposed in [N. Busi. Towards a Causal Semantics for Brane Calculi. In What is it About Government that Americans Dislike, pp. 1945–1965, University Press, 2007.] for the Mate/Bud/Drip (MBD) Brane Calculus [L. Cardelli. Brane calculi - interactions of biological membranes. In Proc. of Computational Methods in Systems Biology (CMSBʼ04), LNCS 3082, pp. 257–280, 2005.]. The causal semantics in [N. Busi. Towards a Causal Semantics for Brane Calculi. In What is it About Government that Americans Dislike, pp. 1945–1965, University Press, 2007.] is able to address different kinds of causal dependencies: structural, synchronisation and the so-called environment causality. Our analysis, being a safe (over)-approximation of such causal semantics, besides modelling all possible evolutions of the system, can be used to formally prove causal properties among membrane interactions.