A tool for the reconstruction of gene regulatory networks from time series data

Reverse engineering of gene regulatory relationships from genomics data is a crucial task to dissect the complex underlying regulatory mechanism occurring in a cell. From a computational point of view the reconstruction of gene regulatory networks is an undetermined problem as the large number of possible solutions is typically high in contrast to the number of available independent data points.  We propose a novel algorithm implemented in a tool based on formal methods, mathematically rigorous techniques widely adopted in engineering to specify and verify complex software and hardware systems. The tool starts with a formal specification of gene regulatory hypotheses and is able to mathematically prove whether a time course experiment belongs or not to the formal specification, determining in fact whether a gene-gene regulation exists or not. The tool is able to detect both direction and sign (inhibition/activation) of regulations whereas most of literature methods are limited to undirected and/or unsigned relationships.


  • Windows 7 or a Linux distribution.
  • Concurrency Workbench of the New Century.

You can’t use it on MacOSX due to the lack of Concurrency Workbench!

Getting started

Install Concurrency Workbench of the New Century ( for your platform. Note: you have to install it in cwb-nc folder (DO NOT MODIFY standard installation paths). You can also employ the RECOMMENDED embedded CWB version if you are under Linux. If you have trouble using it on a x86_64 machine, please install ia32 libs. 


java -jar formalM.jar timeseries perturbations discretized_timeseries [yes/no]

Timeseries and perturbations are the input files respectively of time series and perturbations. Discretized_timeseries is the input file of the discretised timeseries. Add “yes” to employ the embedded CWB for formal verification. Otherwise FormalM will use your standard CWB installation.



Soon the tool will be available as a plugin for the genome workbench (