"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis

BMC Bioinformatics

Software

Mariana Benítez¹  David A Rosenblueth²  Elena R Alvarez-Buylla³  Eugenio Azpeitia³  Pedro Góngora⁴  Julián Argil⁴  Miguel Carrillo⁴  Gustavo Arellano⁴ 

[1] Centro de Ciencias de la Complejidad, piso 6, ala norte, Torre de Ingeniería, Universidad Nacional Autónoma de México, Coyoacán, 04510, México D.F, México;Department of Functional Genomics and Proteomics, Masaryk University, Kotlářská 2, CZ-61137, Brno, Czech Republic;CEITEC-Central European Institute of Technology, Masaryk University, Žerotínovo nám. 9, CZ-60177, Brno, Czech Republic;Centro de Ciencias de la Complejidad, piso 6, ala norte, Torre de Ingeniería, Universidad Nacional Autónoma de México, Coyoacán, 04510, México D.F, México;Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México, Apdo. Postal 20-726, 01000, México D.F, México;Centro de Ciencias de la Complejidad, piso 6, ala norte, Torre de Ingeniería, Universidad Nacional Autónoma de México, Coyoacán, 04510, México D.F, México;Laboratorio de Genética Molecular, Desarrollo y Evolución de Plantas, Instituto de Ecología, Universidad Nacional Autónoma de México, 3er Circuito Universitario Exterior, Junto al Jardín Botánico, Coyoacán, 04510, México D.F, México;Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México, Apdo. Postal 20-726, 01000, México D.F, México;

关键词: Model Checker;    Boolean Function;    Truth Table;    Stem Cell Niche;    Stable Steady State;   

DOI  :  10.1186/1471-2105-12-490

 received in 2011-05-31, accepted in 2011-12-22,  发布年份 2011

来源: Springer

【 摘 要 】

BackgroundIn Thomas' formalism for modeling gene regulatory networks (GRNs), branching time, where a state can have more than one possible future, plays a prominent role. By representing a certain degree of unpredictability, branching time can model several important phenomena, such as (a) asynchrony, (b) incompletely specified behavior, and (c) interaction with the environment. Introducing more than one possible future for a state, however, creates a difficulty for ordinary simulators, because infinitely many paths may appear, limiting ordinary simulators to statistical conclusions. Model checkers for branching time, by contrast, are able to prove properties in the presence of infinitely many paths.ResultsWe have developed Antelope ("Analysis of Networks through TEmporal-LOgic sPEcifications", http://turing.iimas.unam.mx:8080/AntelopeWEB/), a model checker for analyzing and constructing Boolean GRNs. Currently, software systems for Boolean GRNs use branching time almost exclusively for asynchrony. Antelope, by contrast, also uses branching time for incompletely specified behavior and environment interaction. We show the usefulness of modeling these two phenomena in the development of a Boolean GRN of the Arabidopsis thaliana root stem cell niche.There are two obstacles to a direct approach when applying model checking to Boolean GRN analysis. First, ordinary model checkers normally only verify whether or not a given set of model states has a given property. In comparison, a model checker for Boolean GRNs is preferable if it reports the set of states having a desired property. Second, for efficiency, the expressiveness of many model checkers is limited, resulting in the inability to express some interesting properties of Boolean GRNs.Antelope tries to overcome these two drawbacks: Apart from reporting the set of all states having a given property, our model checker can express, at the expense of efficiency, some properties that ordinary model checkers (e.g., NuSMV) cannot. This additional expressiveness is achieved by employing a logic extending the standard Computation-Tree Logic (CTL) with hybrid-logic operators.ConclusionsWe illustrate the advantages of Antelope when (a) modeling incomplete networks and environment interaction, (b) exhibiting the set of all states having a given property, and (c) representing Boolean GRN properties with hybrid CTL.

【 授权许可】

Unknown   
© Arellano et al.; licensee BioMed Central Ltd. 2011. This article is published under license to BioMed Central Ltd. This is an open access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/2.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.