"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis
<p>Abstract</p> <p>Background</p> <p>In Thomas' formalism for modeling gene regulatory networks (GRNs), <it>branching time</it>, where a state can have <it>more than one possible future</it>, plays a prominent role. By representing a certain...
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
BMC
2011-12-01
|
| Series: | BMC Bioinformatics |
| Online Access: | http://www.biomedcentral.com/1471-2105/12/490 |
| _version_ | 1828774535844855808 |
|---|---|
| author | Arellano Gustavo Argil Julián Azpeitia Eugenio Benítez Mariana Carrillo Miguel Góngora Pedro Rosenblueth David A Alvarez-Buylla Elena R |
| author_facet | Arellano Gustavo Argil Julián Azpeitia Eugenio Benítez Mariana Carrillo Miguel Góngora Pedro Rosenblueth David A Alvarez-Buylla Elena R |
| author_sort | Arellano Gustavo |
| collection | DOAJ |
| description | <p>Abstract</p> <p>Background</p> <p>In Thomas' formalism for modeling gene regulatory networks (GRNs), <it>branching time</it>, where a state can have <it>more than one possible future</it>, 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 <it>infinitely many </it>paths may appear, limiting ordinary simulators to statistical conclusions. <it>Model checkers </it>for branching time, by contrast, are able to prove properties in the presence of infinitely many paths.</p> <p>Results</p> <p>We have developed <it>Antelope </it>("Analysis of Networks through TEmporal-LOgic sPEcifications", <url>http://turing.iimas.unam.mx:8080/AntelopeWEB/</url>), a model checker for analyzing and constructing Boolean GRNs. Currently, software systems for Boolean GRNs use branching time almost exclusively for asynchrony. <it>Antelope</it>, 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 <it>Arabidopsis thaliana </it>root stem cell niche.</p> <p>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 <it>given </it>set of model states has a given property. In comparison, a model checker for Boolean GRNs is preferable if it <it>reports </it>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.</p> <p><it>Antelope </it>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.</p> <p>Conclusions</p> <p>We illustrate the advantages of <it>Antelope </it>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.</p> |
| first_indexed | 2024-12-11T15:22:58Z |
| format | Article |
| id | doaj.art-2ff47e46cca44c808753ea1bac905f96 |
| institution | Directory Open Access Journal |
| issn | 1471-2105 |
| language | English |
| last_indexed | 2024-12-11T15:22:58Z |
| publishDate | 2011-12-01 |
| publisher | BMC |
| record_format | Article |
| series | BMC Bioinformatics |
| spelling | doaj.art-2ff47e46cca44c808753ea1bac905f962022-12-22T01:00:18ZengBMCBMC Bioinformatics1471-21052011-12-0112149010.1186/1471-2105-12-490"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysisArellano GustavoArgil JuliánAzpeitia EugenioBenítez MarianaCarrillo MiguelGóngora PedroRosenblueth David AAlvarez-Buylla Elena R<p>Abstract</p> <p>Background</p> <p>In Thomas' formalism for modeling gene regulatory networks (GRNs), <it>branching time</it>, where a state can have <it>more than one possible future</it>, 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 <it>infinitely many </it>paths may appear, limiting ordinary simulators to statistical conclusions. <it>Model checkers </it>for branching time, by contrast, are able to prove properties in the presence of infinitely many paths.</p> <p>Results</p> <p>We have developed <it>Antelope </it>("Analysis of Networks through TEmporal-LOgic sPEcifications", <url>http://turing.iimas.unam.mx:8080/AntelopeWEB/</url>), a model checker for analyzing and constructing Boolean GRNs. Currently, software systems for Boolean GRNs use branching time almost exclusively for asynchrony. <it>Antelope</it>, 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 <it>Arabidopsis thaliana </it>root stem cell niche.</p> <p>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 <it>given </it>set of model states has a given property. In comparison, a model checker for Boolean GRNs is preferable if it <it>reports </it>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.</p> <p><it>Antelope </it>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.</p> <p>Conclusions</p> <p>We illustrate the advantages of <it>Antelope </it>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.</p>http://www.biomedcentral.com/1471-2105/12/490 |
| spellingShingle | Arellano Gustavo Argil Julián Azpeitia Eugenio Benítez Mariana Carrillo Miguel Góngora Pedro Rosenblueth David A Alvarez-Buylla Elena R "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis BMC Bioinformatics |
| title | "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis |
| title_full | "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis |
| title_fullStr | "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis |
| title_full_unstemmed | "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis |
| title_short | "Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis |
| title_sort | antelope a hybrid logic model checker for branching time boolean grn analysis |
| url | http://www.biomedcentral.com/1471-2105/12/490 |
| work_keys_str_mv | AT arellanogustavo antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT argiljulian antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT azpeitiaeugenio antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT benitezmariana antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT carrillomiguel antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT gongorapedro antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT rosenbluethdavida antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis AT alvarezbuyllaelenar antelopeahybridlogicmodelcheckerforbranchingtimebooleangrnanalysis |