Infer gene regulatory networks from time series data with formal methods

Reverse engineering of regulatory relationships from genomics data is emerging as crucial to dissect the complex underlying regulatory mechanism occurring in a cell. In this paper we propose a novel reverse engineering algorithm that makes use of formal methods, usually adopted in engineering to specify and verify concurrent software and hardware systems. With a formal specification of gene regulatory hypotheses we are able to prove mathematically whether a time course experiment belongs or not to the formal specification, determining in fact whether a gene regulation exists or not. The method is capable to detect both direction and sign (inhibition/activation) of regulations whereas most of literature methods which are limited to undirected and/or unsigned relationships. The method, empirically evaluated on experimental and synthetic datasets, reaches high levels of accuracy, outperforming literature methods in terms of precision and recall, despite the computational cost increases exponentially with the size of the network.