Reachability analysis of biological signalling pathways by abstract interpretation

International audienceAgent-based formal languages can be used to describe biological signalling networks. As for any language, this process is error prone. Thus we require static analysis tools to check whether the formal description of models matches with what the programmer (or the biologist) has in mind. However, biological networks involve a large number of non-isomorphic complexes (i.e.~the number of non-isomorphic ways in which agents can connect), as a consequence static analyses must cope with this combinatorial blow up. We use the abstract interpretation framework, which is a theory of semantics approximation, to design an abstraction of the set of reachable complexes. This abstraction is both accurate and efficient. Then we show several applications. First, we use this abstraction to detect some bugs such as dead reactions (reactions that can never be triggered) and conflicting rules (distinct rules that compute the same thing). Our analysis also predicts whether two sites may bind in any context, or if this binding is controlled by other sites