Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México, 01000 México D.F., México.
BMC Bioinformatics. 2011 Dec 22;12:490. doi: 10.1186/1471-2105-12-490.
In 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.
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.
在托马斯（Thomas）用于建模基因调控网络（GRN）的形式化方法中，分支时间（其中一个状态可以有多个可能的未来）起着重要作用。通过表示一定程度的不可预测性，分支时间可以建模几个重要现象，例如（a）异步，（b）不完全指定的行为，以及（c）与环境的交互。为一个状态引入多个可能的未来会给普通模拟器带来困难，因为可能会出现无限数量的路径，从而限制普通模拟器做出统计结论。相比之下，分支时间的模型检查器能够在存在无限数量的路径的情况下证明属性。
我们开发了 Antelope（“Analysis of Networks through TEmporal-LOgic sPEcifications”，http://turing.iimas.unam.mx:8080/AntelopeWEB/），这是一种用于分析和构建布尔型 GRN 的模型检查器。目前，用于布尔型 GRN 的软件系统几乎完全将分支时间用于异步。相比之下，Antelope 还将分支时间用于不完全指定的行为和环境交互。我们展示了在开发拟南芥根干细胞生态位的布尔型 GRN 时，对这两种现象进行建模的有用性。在将模型检查直接应用于布尔型 GRN 分析时，存在两个障碍。首先，普通模型检查器通常仅验证给定模型状态集是否具有给定属性。相比之下，如果模型检查器能够报告具有所需属性的状态集，则更适合用于布尔型 GRN。其次，为了提高效率，许多模型检查器的表达能力受到限制，导致无法表达布尔型 GRN 的某些有趣属性。Antelope 试图克服这两个缺点：除了报告具有给定属性的所有状态集之外，我们的模型检查器还可以表达一些普通模型检查器（例如 NuSMV）无法表达的属性，以牺牲效率为代价。这种额外的表达能力是通过使用扩展标准计算树逻辑（CTL）的混合逻辑运算符来实现的。
当（a）对不完整网络和环境交互进行建模，（b）展示具有给定属性的所有状态集，以及（c）用混合 CTL 表示布尔型 GRN 属性时，我们说明了 Antelope 的优势。
