A Control Flow Analysis for Beta-binders with and without static compartments

We introduce a Control Flow Analysis, that statically approximates the dynamic behaviour of processes, expressed in the Beta-binders calculus and in an extended version of the calculus modelling static compartments. Our analysis of a system is able to describe the essential behaviour of each box, tracking all the possible bindings of variables, all the possible intra- and inter-boxes communications, and, finally, all the possible movements across compartments. The analysis offers a basis for establishing static checks of biological dynamic properties. We apply our analysis to an abstract specification of the interaction between a virus and cells of the immune system and to a model of the cAMP-signaling Pathway in Olfactory Sensory Neurons.