Causal static analysis for Brane Calculi

We present here a static analysis, based on Abstract Interpretation [8], obtained by defining an abstract version of the causal semantics for the Mate/Bud/Drip (MBD) version of Brane Calculi [7], proposed by Busi [6]. Our analysis statically approximates the dynamic behaviour of MBD systems. More precisely, the analysis is able to describe the essential behaviour of the represented membranes, in terms of their possible interactions. Furthermore, our analysis is able to statically capture the possible causal dependencies among interactions, whose determination can be exploited to better understand the modelled biological phenomena. Finally, we apply our analysis to an abstract specification of the receptor-mediated endocytosis mechanism.