a1 LUNAM Université, École Centrale de Nantes, IRCCyN UMR CNRS 6597 (Institut de Recherche en Communications et Cybernétique de Nantes), 1 rue de la Noë - B.P. 92101 - 44321 Nantes Cedex 3, France and LIX, École Polytechnique, 91128 Palaiseau Cedex, France Email: firstname.lastname@example.org
a2 LUNAM Université, École Centrale de Nantes, IRCCyN UMR CNRS 6597 (Institut de Recherche en Communications et Cybernétique de Nantes), 1 rue de la Noë - B.P. 92101 - 44321 Nantes Cedex 3, France Email: email@example.com; firstname.lastname@example.org
The analysis of the 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 Process Hitting, which is a framework suitable for modelling dynamical complex systems. In particular, Process Hitting has been shown to be of interest in providing compact models of the dynamics of BRNs with discrete values. Process Hitting splits a finite number of processes into so-called sorts and describes the way each process is able to act upon (that is, to ‘hit’) another one (or itself) in order to ‘bounce’ it as another process of the same sort with further actions.
By using complementary abstract interpretations of the succession of actions in Process Hitting, we build a very efficient static analysis to over- and under-approximate reachability properties, which avoids the need to build the underlying states graph. The analysis is proved to have a low theoretical complexity, in particular when the number of processes per sorts is limited, while a very large number of sorts can be managed.
This makes such an approach very promising for the scalable analysis of abstract complex systems. We illustrate this through the analysis of a large BRN of 94 components. Our method replies quasi-instantaneously to reachability questions, while standard model-checking techniques regularly fail because of the combinatoric explosion of behaviours.
(Received March 07 2011)
(Revised December 12 2011)
(Online publication May 08 2012)