Tutorial

Overview

Studying the behaviour of dynamic biological systems is made by model checking; this method generates scenarios based on the constraints defined in a model. A scenario or a trajectory (i.e. a sequence of states of biomolecules), can be described with the help of propositional logic formulas.

A SAT solver allows us to analyse constraints from models with several thousands of places and transitions. It is used to either give a satisfiability answer, or generate a set of initial activation states for the boundaries (frontier places) of the system. Cadbiom uses the free and open source CryptoMinisat solver [CryptoMiniSat] which happens to be a winner of the 2010 and 2015 SAT Race competitions [SAT-Race2015].

Cadbiom has benefited from a major refactoring over the years. Some particularly costly functions in calculation time have been written in C. An architecture implementing multiprocessing technology has been integrated into the command line module to take advantage of the computing power of modern computers and distributed computing infrastructures. Moreover, an increased computing capacity has been achieved thanks to last versions of CryptoMinisat.

We can thus compare the performance of the old Cadbiom versions with the new one in terms of the number of solutions obtained per unit of time.

Improved performance over the development years (log scale for y axis). Tested on monoprocess usage on the following hardware configuration: CPU: i7-3630QM, 3.2GHz; Memory: 12 Go DDR3-RAM PC3-12800. Query: SRP9 molecule; Model: Whole NCI-PID database translated into CADBIOM formalism(and).bcx.

The modules

While the graphical interface of Cadbiom is the easiest way to explore small models, the command line is a must-have for larger models with several hundred of entities.

The GUI provides a graph editor to build and explore models; it purposes a simple query interface to analyse the dynamics of a model (i.e. search properties and conduct discrete time simulations).

The command line module allows searching trajectories, and necessary and sufficient sets of boundaries related to the states of the places of interest mentioned in a logical formula built by the user. These sets are also called Minimal Activation Conditions.

Output files from Cadbiom can be difficult to exploit by hand (See Cadbiom File Format Specification); they contain the sequences of transitions necessary to satisfy a problem. We have developed sub commands that allow to work with these files from the command line.

We are thus able to generate trajectory graphs from boundaries to entities of interest. These graphs can be opened in applications such as Cytoscape or Gephi. We can also compare trajectories with each other and generate matrices of occurrences of places and heatmaps. We can work with the models to extract information and easily know their content.

Examples of uses are described in the next chapter.