Abstraction and Verification of Large-scale Biological Networks

Biological networks can be modelled as automata networks where each automaton represents a biological component with a few local states (e.g., active/inactive). Due to the combinatorial explosion of the state space, the verification of dynamical properties (fixed points, reachability, attractors, ..) is very challenging when applied to large-scale systems.

I'll introduce a restriction of asynchronous automata networks, the Process Hitting, upon which efficient over- and under-approximation of reachability properties have been designed. These approximations rely on a dedicated abstract interpretation framework which highlights some aspects of the causality between the reachability of local states of automata. The complexity of the approximated verification is polynomial in the number of automata and exponential in the number of local states within one automata, which makes it tractable for the analysis of very large biological networks.

In addition, the presented causality analysis allows to efficiently derive local states of automata whose presence is necessary for the occurrence of a given reachability property. Applied to biological models, such cut sets provide potential therapeutic targets.

These results are illustrated with applications to Boolean models of signalling and regulatory networks, ranging from 100 to more than 9000 interacting components.