The study of biological networks has led to the development of increasingly large and detailed models. While whole-cell models are not on the horizon yet, complex networks underlying specific cellular processes have been modeled in detail. The study of these models by means of analysis and simulation tools leads to large amounts of predictions, typically time-courses of the concentration of several dozens of molecular components in a variety of physiological conditions and genetic backgrounds. This raises the question how to make sense of these simulations, that is, how to obtain an understanding of the way in which particular molecular mechanisms control the cellular process under study, and how to identify interesting predictions of novel phenomena that can be confronted with experimental data. Formal verification techniques based on model-checking provide a powerful technology to keep up with this increase in scale and complexity. The basic idea underlying model checking is to specify dynamical properties of interest as statements in temporal logic, and to use model-checking algorithms to automatically and efficiently verify whether the properties are satisfied or not by the model. The application of model-checking techniques is hampered, however, by several key issues described in this thesis. First, the systems biology domain brought to the fore a few properties of the network dynamics that are not easily expressed using classical temporal logics, like Computation Tree Logic (Ctl) and Linear Time Logic (Ltl). On the one hand, questions about multistability are important in the analysis of biological regulatory networks, but difficult (or impossible) to express in Ltl. On the other hand, Ctl is capable of dealing with branching time, important for multistability and other properties of non-deterministic models, but it does not do a good job when faced with questions about cycles in a Kripke structure. Second, the problem of posing relevant and interesting questions is critical in modeling in general, but even more so in the context of applying model-checking techniques, due to the fact that it is not easy for non-experts to formulate queries in temporal logic. Finally, most of the existing modelling and simulation tools are not capable of applying model-checking techniques in a transparent way. In particular, they do not hide from the user the technical details of the installation of the model checker, the export in a suitable format of the model and the query, the call of the model checker, and the import of the results produced by the model checker (the true/false verdict and witness/counterexample). This report starts by describing the basic concepts for formal verification, introducing the necessary data structures that represent the possible behaviors of a dynamical system, as well as the different types of temporal logics necessary for the encoding the properties. It also presented the generic model checking problem, which consists in determining if a given system satisfies a given set of properties. Some recent examples of the application of model checking techniques in system biology are also presented, as well as the current problems and limitations that need to be addressed. Finally, some concluding remarks are presented pointing some directions towards a better integration between the formal verification and the systems biology fields.

Location(s)