J 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.

Základní údaje

Originální název

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

Autoři

ARELLANO, Gustavo (484 Mexiko), Julián ARGIL (484 Mexiko), Eugenio AZPEITIA (484 Mexiko), Mariana BENITEZ (484 Mexiko, domácí), Miguel CARRILLO (484 Mexiko), Pedro GONGORA (484 Mexiko), David A. ROSENBLUETH (484 Mexiko) a Elena R. ALVAREZ-BUYLLA (484 Mexiko, garant)

Vydání

BMC BIOINFORMATICS, UK, Springer, 2011, 1471-2105

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

Genetika a molekulární biologie

Stát vydavatele

Velká Británie a Severní Irsko

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Impakt faktor

Impact factor: 2.751

Kód RIV

RIV/00216224:14740/11:00055435

Organizační jednotka

Středoevropský technologický institut

DOI

UT WoS

000302435200001

Klíčová slova anglicky

boolean network; model checking; root apical meristem

Štítky

Příznaky

Mezinárodní význam
Změněno: 26. 3. 2012 22:40, Olga Křížová

Anotace

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.

Návaznosti

LC06034, projekt VaV
Název: Regulace morfogeneze rostlinných buněk a orgánů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Regulace morfogeneze rostlinných buněk a orgánů