Detailed Information on Publication Record
2011
"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis
ARELLANO, Gustavo, Julián ARGIL, Eugenio AZPEITIA, Mariana BENITEZ, Miguel CARRILLO et. al.Basic information
Original name
"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis
Authors
ARELLANO, Gustavo (484 Mexico), Julián ARGIL (484 Mexico), Eugenio AZPEITIA (484 Mexico), Mariana BENITEZ (484 Mexico, belonging to the institution), Miguel CARRILLO (484 Mexico), Pedro GONGORA (484 Mexico), David A. ROSENBLUETH (484 Mexico) and Elena R. ALVAREZ-BUYLLA (484 Mexico, guarantor)
Edition
BMC BIOINFORMATICS, UK, Springer, 2011, 1471-2105
Other information
Language
English
Type of outcome
Článek v odborném periodiku
Field of Study
Genetics and molecular biology
Country of publisher
United Kingdom of Great Britain and Northern Ireland
Confidentiality degree
není předmětem státního či obchodního tajemství
References:
Impact factor
Impact factor: 2.751
RIV identification code
RIV/00216224:14740/11:00055435
Organization unit
Central European Institute of Technology
UT WoS
000302435200001
Keywords in English
boolean network; model checking; root apical meristem
Tags
International impact
Změněno: 26/3/2012 22:40, Olga Křížová
Abstract
V originále
We 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. We 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.
Links
| LC06034, research and development project |
|