Static Analysis by Abstract Interpretation of Biological Regulatory Networks Dynamics

The analysis of dynamics of Biological Regulatory Networks (BRNs) requires innovative methods to cope with the state space explosion. This paper settles an original approach for deciding reachability properties based on the Process Hitting, a framework suitable to model dynamical complex systems. In particular, the Process Hitting has been shown of interest to model dynamics of BRNs with discrete values. The Process Hitting describes the way each process is able to act upon (i.e. to "hit") an other one (or itself) in order to "bounce" it as another process further acting. By using complementary abstract interpretations of the succession of actions, we build a very efficient static analysis to over- and under-approximate reachability properties within Process Hittings. Applied to a large BRN of 94 components, our method replies quasi-instantaneously to reachability questions, overtaking the state-of-the-art approaches and showing a very promising scalability