BACKGROUND
gene regulatory network models
a major challenge in current biology is relating spatio-temporal gene expression patterns to phenotypic traits of an organism.
these patterns result partly from complex regulatory interactions sustained principally by genes and encoded proteins.
the complexity of such interactions exceeds the human capacity for analysis.
thus, mathematical and computational models of gene regulatory networks  are indispensable tools for tackling the problem of mapping the genotype into the phenotype.
these models have been fruitfully applied in numerous biological systems .
within the various kinds of grn models  <cit> , boolean grns are especially valuable for their simplicity and for nonetheless having a rich behavior yielding meaningful biological information  <cit> .
examples where boolean grns have been successfully used are: the segment polarity gene network of drosophila melanogaster  <cit> , the flower organ determination grn of arabidopsis thaliana  <cit> , the mammalian cell cycle  <cit> , and the yeast cell cycle  <cit> .
in a boolean grn, each gene has only two possible activation values: active  or inactive ; intermediate expression levels are neglected.
a network state at time t is a vector containing the activation values of all the genes in the grn at time t. in addition, time is viewed as proceeding in discrete steps.
the value of every gene x at time t +  <dig> is specified by a boolean function of the values of its regulators g <dig> g <dig> …,gnx at time t.
branching time
boolean grns are closely related to the formalism developed by thomas and his collaborators  <cit> .
thus, computer systems for boolean grns are often influenced by thomas' formalism, which employs grn models with branching time, allowing states with more than one immediate future .
a network state with more than one immediate future represents the fact that the next state of the regulatory system modeled by such a grn can be any one of several states.
hence, the next state of the modeled system is only partially determined.
let us then say that there is an indetermination in the network.
this indetermination in the system's behavior reflects a certain degree of unpredictability that can be identified with several important phenomena.
asynchrony
one such phenomenon is asynchrony .
experiments for inferring gene interaction do not normally establish the length of time between state changes.
hence, when such experiments indicate the change in value of two genes, say, it is preferable to model such a situation with a single state having two successors, one for each change, as illustrated in figure  <dig>  the reasons are that we do not know the relative values of both delays in real biological systems  and that complete synchrony might be practically impossible .
many computer systems based on, or inspired by, thomas' formalism  employ asynchronous models.
thomas' formalism, however, incorporates two additional phenomena with indeterminations, that are typically excluded in such systems.
incompletely specified behavior
one such additional phenomenon is incompletely specified behavior .
this behavior may emerge, first, from a "synthetic" approach , where we are interested in all boolean grns having certain properties  regardless of other properties.
the tables specifying the network behavior would then have outputs whose value "does not matter" .
second, lack of some of the experimental information of a regulatory system also emerges as incompletely specified behavior.
in this case, the behavior tables would have outputs whose value we do not know.
interaction with the environment
another phenomenon usually neglected in computer systems for grn analysis and that can be modeled with branching time is that of interaction with the environment.
assume that the next state of a regulatory system depends on the temperature: if the temperature is low, the system's next state will be one, but if the temperature is high, the system's next state will be different.
another example is the unpredictability of radiation-induced apoptosis  <cit> .
in this case, for the same degree of radiation some cells will initiate apoptosis while others will not.
thomas and d'ari reflect such an unpredictability with an "input variable"  of an unknown value.
this phenomenon can be readily incorporated with indeterminations.
simulators
boolean grns are sometimes studied with simulators .
a simulator attempts to replicate the behavior of a system by performing state changes in the same order as they occur in the system being modeled.
hence, network paths are traversed forward from one state to the next.
in the presence of a state with more than one successor, such a straightforward approach must be complemented with additional mechanisms.
two of such mechanisms are:  a random device  and  backtracking  coupled with a cycle-detection mechanism.
a random device, on the one hand, allows for only drawing statistical conclusions.
the reason is that in the presence of a state with more than one successor, the number of paths may be infinite  <cit> , as depicted in figure  <dig>  backtracking and cycle detection, on the other hand, can be inefficient .
there are two important approaches for circumventing these difficulties.
one of these techniques is an elaboration of backtracking so as to increase its efficiency by requiring certain constraints to be satisfied as the network is traversed  <cit> .
the work by corblin et al.
<cit>  uses this approach.
another relevant method is model checking.
model checking
model checking  <cit>  is a collection of techniques for automatically verifying properties especially of discrete systems.
the main ideas of model checking appeared  <dig> years ago  <cit> .
at present, numerous model-checking tools exist.
model checking is routinely used, mainly for hardware verification, but also for software verification  <cit> , and was distinguished with the a. m. turing award in  <dig>  model checking has been advocated for analyzing biological systems with increasing interest  <cit> .
a model checker normally has as input  a "kripke structure" representing a discrete system ,  a distinguished "initial" state  in the kripke structure, and  a "temporal-logic" formula expressing a desirable property, that may or may not hold  at a state.
the output of the model checker is either a confirmation or a denial that the formula holds at the initial state .
in a kripke structure time is branching, so that there may be more than one possible future of a given state.
the introduction of branching time may produce infinitely many forward traversals .
model checkers, however, unlike simulators randomly selecting a successor state, can systematically analyze such infinitely many possibilities  <cit> .
intuitively, this is often done by traversing the kripke structure in reverse and accumulating the set of all states at which a subformula holds.
model checking amounts, thus, to performing an exhaustive search .
such a search plays the role of a mathematical proof establishing a property for infinitely many paths.
programming vs. formula writing
by being based on properties formalized in temporal logic, model checkers have another advantage over simulators.
the decision of whether or not a state satisfies a property of interest is programmed in the simulator itself.
therefore, if an unforeseen property appears during the usage of a boolean grn simulator, such a property must be incorporated in the simulator by modifying program code.
this renders simulators rigid: either the user's needs are anticipated or reprogramming must be done.
compared with simulators, model checkers exhibit the benefit of having replaced programming with temporal-logic formula writing.
instead of having to modify the computer program of a simulator, many new queries can be dealt with by writing new temporal-logic formulas , which  are concise and self-contained.
organization of this paper
in the implementation section, we first illustrate both computation-tree logic   <cit>  and its hybrid extension, hybrid ctl , chosen to be able to express interesting properties for boolean grn analysis and construction.
the term "hybrid" here means a combination of propositional modal logic with classical predicate logic, and should not to be confused with hybrid model checking, combining discrete with continuous variables.
the implementation section subsequently covers the model-checking algorithms and some implementation details.
next we show, in the results section, the use of the antelope model checker in the presence of indeterminations either caused by environment interaction or by an incompletely specified behavior.
finally, the discussion section reviews other similar software systems, compares antelope with such systems, and outlines features planned for the future.
implementation
this section first covers the temporal logics used by antelope.
after explaining ctl, we turn our attention to its hybrid extension.
next, we cover the model-checking algorithms, as well as additional implementation issues.
computation-tree logic
we now give a short account of ctl and refer the reader to additional file  <dig> of this paper for a gentle introduction and to additional file  <dig> for a formal definition of ctl.
more thorough treatments can be found in  <cit> .
boolean and temporal operators
formulas in ctl can have boolean operators, such as not and or.
in addition, such formulas can have "temporal operators", allowing us to refer to formulas holding in the future of a particular state.
in this case, we must indicate whether we mean some future or all futures.
hence, it is possible to refer either  to some path starting in the present with the "modality" e, or  to all paths starting in the present with the modality a. similarly, it is possible to refer  to the immediate future with the modality x,  to any state in the present or any point in the future with the modality f, or  to all states in the present and in the future with the modality g. table  <dig> summarizes these modalities.
a temporal operator is composed of a modality in the upper part together with a modality in the lower part of this table, which results in six temporal operators.
for example, a formula asserting that there exists a path such that in the present or in the future g <dig> does not hold  and g <dig> does hold  would be: "ef and g1)".
hence, assuming that there is a single state s in which g <dig> does not hold and g <dig> does hold, this formula can be used to obtain the basin of attraction of such a state, with a model checker computing all states at which a given formula holds.
the formula "ax  and g1)" holds at all states from which it is necessary to reach s in one step, i.e., states which have s as their only next state.
the formula "ex  and g1)" holds at all states from which it is possible to reach s in one step, i.e., states which have s as a next state .
other ctl formulas can characterize, for instance, whether or not it is necessary to go through a state s <dig> to reach another state s <dig>  see  <cit>  for a list of ctl formulas specifying various biological properties.
some properties not expressible in ctl
there do not exist, however, ctl formulas for characterizing steady states   <cit> , or oscillations.
this motivates the use of a more expressive logic than ctl.
antelope provides a "hybrid" extension of ctl.
hybrid computation-tree logic
this subsection is devoted to hybrid ctl.
we refer the reader to additional file  <dig> of this paper for a gentle introduction and to additional file  <dig> for a formal definition of hybrid ctl.
deeper treatments of hybrid logics are in  <cit> .
state variables
the main idea behind the hybrid extension of a temporal logic consists in the addition of variables allowing us to refer to states .
the downarrow binder "↓σ" sets the state variable σ to the current state of evaluation.
the formula "↓σ.ax σ", for example, characterizes the set of states which have themselves as their only next state.
hence, hybrid ctl allows us to characterize the set of steady states.
moreover, by employing branching time, we are able to distinguish between two kinds of steady state.
when a state has only one transition from and to itself, following thomas and d'ari  <cit> , we will call it a stable steady state.
when a state has, in addition to a self-loop, other transitions going to other states, following  <cit> , we will call it an unstable steady state .
hybrid ctl formulas for calculating both these sets of states are: "↓σ.ax σ", for the set of stable steady states, and "↓σ.exσ", for the union of the sets of stable and unstable steady states.
other formulas
attractors of various sizes and oscillations
the notion of a steady state can be generalized in an attractor, possibly involving more than one state.
a steady state would then be a one-state attractor.
a formula characterizing attractors of any size would be: "↓σ.ex ef σ".
another interesting formula would be "↓σ.ex and ex σ)", which holds at states belonging to a size-two attractor.
oscillations, where a gene is alternatively active and inactive, can also be characterized in hybrid ctl: additional file  <dig> explains a formula for the basin of attraction of possible oscillations.
we refer the reader to the antelope web site http://turing.iimas.unam.mx:8080/antelopeweb/ for more formulas.
algorithms
ctl
antelope uses a standard "labeling" algorithm  <cit>  for ordinary ctl formulas.
labeling algorithms for model checking are so called because we can think of each state as being labeled with the subformulas holding at that state.
say that the formula given by the user is φ. the labeling algorithm starts by considering the simplest subformulas of φ, that is, the names of the genes.
for each gene g, labeling all states at which the formula "g" holds is easy, as that information is already present in the kripke structure.
next, the labeling algorithm proceeds to more complex subformulas, until φ is reached, by treating the operator of each such subformula by cases.
for instance, if the subformula is of the form "ψ <dig> and ψ2", then the labeling algorithm computes the set of states at which such a subformula holds as the intersection of the set of states at which ψ <dig> holds with the set of states at which ψ <dig> holds.
all boolean operators can be treated by combining set operations, like union, intersection, and set difference.
the labeling algorithm treats some temporal operators, such as ax, by using equivalences.
for example, "ax ψ" is equivalent to "not ex not ψ".
the rest of the temporal operators, however, must be dealt with explicitly.
for all such primitive operators the labeling algorithm traverses the kripke structure in reverse.
take for instance "ex ψ", which holds if there exists a next state at which ψ holds.
given the set of states at which ψ holds, the labeling algorithm treats "ex ψ" by obtaining all states which have an immediate successor in such a set, i.e., all the predecessors of the states in such a set.
the labeling algorithm processes operators such as eg by repetitively traversing the kripke structure in reverse.
hybrid ctl
the labeling algorithm is efficient .
the additional expressiveness of hybrid operators, such as "↓" comes at a price, however.
given a ctl formula φ, the computation of the set of states at which a formula of the form "↓σ.φ" holds involves calling the labeling algorithm with φ once for each state.
the decrease in efficiency is even more if the "↓" operator appears nested.
antelope, however, treats certain patterns in special ways, requiring less time than a direct approach.
more implementation issues
antelope is a symbolic model checker  <cit> , representing state sets by reduced, ordered binary-decision diagrams   <cit> .
representation of a set of states
a bdd is a representation of a boolean function.
thus, to use a bdd for representing a set of states in a kripke structure we must view such a set as a boolean function.
this is possible if each row of the truth table of the boolean function corresponds to an element which may or may not belong to such a set.
the value of such a function will be  <dig> at exactly those states belonging to the set.
representation of a set of transitions
in addition to representing sets of states, bdds are used for representing the set of transitions of kripke structures.
in this case, the boolean function has twice as many variables as there are genes.
the reason is that each transition  has both a source and a terminating state.
bdds are often surprisingly concise, allowing the verification of many large kripke structures, with more than  <dig> states  <cit> .
we refer the reader to  <cit>  for a detailed description of bdds and their use in symbolic model checking.
optimizations
apart from the use of bdds, antelope has several "optimizations" .
for example, a straightforward formula characterizing the states with more than one successor has the pattern "↓σ.ex ↓τ.φ".
if evaluated as described in the algorithms section, this formula would call the labeling algorithm a number of times proportional to the square of the number of states , where |s| is the number of states).
to find the set of states with more than one successor, however, it is not necessary to visit all states for each state of the kripke structure.
it suffices to be able to enumerate the successors of each state.
antelope treats the formula for characterizing the states with more than one successor as a special case so that the ctl model-checking algorithm is called with φ as input a number of times linear in the size of the kripke structure , where |r| is the number of transitions).
another optimization is that of the operator ey , which is the converse of ex.
although this operator need not be primitive, antelope does treat it as primitive by simply traversing the transitions forward.
this operator allows the user to view antelope as a kind of simulator.
additional file  <dig> has a table comparing the verification times for a few models with respect to some properties of increasing complexity.
input formats
antelope accepts two formats for describing the boolean grn: tables and equations.
in both cases, the values of a gene  are specified as a boolean relation which depends on the values of  genes .
a table can be viewed as an extension of an ordinary truth table, where stars are allowed on the right-hand side, denoting indeterminations.
sometimes, however, it may be more convenient to use a logical formula instead of a truth table.
hence, antelope accepts equations, each of which is of the form:
x:=fx
where the left-hand side represents the value of the gene x at the current time step, and the right-hand side is an arbitrary boolean function  on the values of genes at the previous time step.
to be able to represent indeterminations, we need two equations with the same left-hand side.
we refer the reader to the antelope user's manual, which appears in additional file  <dig>  and in the url http://turing.iimas.unam.mx:8080/antelopeweb/.
RESULTS
we now exemplify the use of antelope for analyzing boolean variants of the a. thaliana root stem cell niche grn.
stem cells or initials are undifferentiated cells from which particular cell types of the organisms are generated; the microenvironment in which stem cells are located is called the stem cell niche.
anatomically, stem cell niches are conformed by two different cell types, the stem cells themselves, and another cell or group of cells sometimes generically called organizer cells  <cit> .
the organizer cells maintain the stem cells in the undifferentiated state through short-range signals.
understanding how the different cells conforming stem cell niches are specified, as well as how the balance between cell division and cell differentiation is maintained in the niches, is central for understanding the development, growth and regeneration processes occurring in plants and animals.
in particular, plant stem cell niches constitute valuable model systems for studying regenerative and plastic developmental processes, as these organisms grow new organs and structures throughout their life  <cit> .
we focus on the root stem cell niche of a. thaliana, that is located near the root tip and is well characterized at the anatomical and molecular level .
this niche is conformed by the so-called quiescent center , which is in turn conformed by the organizer cells of the root scn, and is surrounded by four different stem cell types  <cit> .
each of these four types of stem cell will give rise to a different cell lineage: vascular, cortex/endodermal, epidermal, and columella/root-cap cells.
however, in this contribution two of the stem cell types  are considered as only one since the available experimental evidence is not enough to distinguish between them at the gene expression level , leaving only four types of initial cells , and epidermal/root-cap  initials).
besides being thoroughly characterized at the anatomical level, the root stem cell niche of a. thaliana has been relatively well described from a molecular and genetic perspective.
indeed, some of the molecular components that are necessary to establish and maintain the root scn cellular patterning have been recently uncovered.
among these components are the genes short-root  and its target gene scarecrow , the immediately downstream genes of the dimer shr/scr, and other genes that interact with them.
another set of relevant genes includes the plethora  genes, which have been proposed to be key components of the molecular readout of the plant hormone auxin.
finally, the qc specific gene wuschel related homeobox <dig>  is fundamental for root scn organization  <cit> ; see the graphical representation of the interactions between these genes in figure  <dig>  moreover, the expression patterns of these genes and the localization of their corresponding proteins have been described.
thus, it is possible to postulate a gene expression profile that characterizes each of the scn cell types mentioned above according to the table  <dig>
in order to define the rules for a boolean grn model for this system, we considered all the genes that have been reported to play a relevant role in the specification of the root stem cells and gathered the available experimental information for the regulation of their expression  <cit> ; see figure  <dig>  these data included mostly molecular genetics experiments, such as experiments with plants containing a mutant allele of a gene.
the resulting rules can be summarized in the following logical statements :
// shr; without regulators
// auxin; without regulators
plt: = arf;
auxins: = auxins;
iaa: = ~ auxins;
arf: = ~ iaa;
shr: = shr;
scr: = shr & scr & ;
jkd: = shr & scr;
mgp: = shr & scr &~ wox;
wox: = arf & shr & scr & ;
as has been proposed for other systems , we expected the stable steady states of our grn model to correspond to the gene expression profiles characterizing the different stem cells within the root niche of a. thaliana .
thus, from our knowledge of the system, we expected four stable steady states.
the expected steady states are indeed obtained after postulating a mutual negative interaction between wox <dig> and mgp, which gives rise to a new testable prediction  <cit> .
using this grn model, we first illustrate the use of indeterminations representing incomplete experimental data.
next, we use indeterminations for modeling the influence of unpredictable external signals.
experimental gap
steady states and scarecrow
while developing the truth tables for this grn, we detected an experimental gap.
we know that scarecrow , a target gene of the dimer shortroot /scr  <cit> , either loses or diminishes its own expression in the jackdaw single mutant  in the stem cell niche  <cit> .
the same is true for scr-dependent quiescent-center marker qc <dig>  <cit> .
the magpie mutant , by contrast, has no visible phenotype.
finally, the mgp jkd double mutant recovers the scr expression  <cit>  .
based on this information, we established the truth table for scr, which appears in table  <dig>  observe the indetermination, reflecting the fact that activity could or could not be lost in a jkd background.
antelope produced three stable steady states, but four unstable steady states .
hence, removing the indetermination in the above table may recover the four expected stable steady states.
we performed the jkd loss-of-function simulation in our models to distinguish which of the two possibilities  recovered the expected states.
interestingly, following the grn state transitions backwards, using the ex operator, we noted that if scr is unable to be expressed in jkd, then neither the wuschel-related homebox <dig>   expression nor the scr expression disappeared at the quiescent-center.
furthermore, our jkd mutant does cause a loss of the cortex-endodermis initials attractor, contrary to what is observed in experimental jkd mutants  <cit> , suggesting that jkd only diminishes scr expression.
again, following the grn transitions backwards for the case in which jkd loss-of-function does not lose scr expression, we found that the system was able to recover the jkd loss-of-function mutant.
based on the result found with the system including indeterminations, we replaced the star by a  <dig> in the table for scr.
once the indetermination was so removed, we obtained four stable steady states.
external signals
fas and scr
let us now exemplify antelope as used for modeling the effect of external signals that affect one or more grn nodes.
the root stem cell niche of a. thaliana is affected by several external signals, such as genes and molecules from modules involved in other processes in the organism.
for example, kaya and collaborators  <cit>  reported that fasciata <dig>  and fasciata <dig> , hereafter collectively called fas, affect scr expression.
in the fas mutant, scr expression is deregulated and can be either expressed or not expressed in almost any cell of the root stem cell niche.
similarly, inagaki and collaborators  <cit>  reported the techbi  mutants also affecting scr expression.
again, when teb is mutated, scr may or may not be expressed through the endodermal layer, the cortex-endodermis initial cells, and the quiescent center.
we incorporated fas by adding a variable fas to the truth table for scr.
for fas =  <dig>  the truth table obtained in the "experimental gap" subsection was used.
for fas =  <dig>  by contrast, all the right-hand sides of the new truth table had indeterminations.
in the case of teb, we only used indeterminations for the right-hand side of the scr table where the output was  <dig> for the teb mutant.
we found that under these conditions the original four attractors were preserved in both cases.
we also found that in the fas mutant, scr could be expressed in any of the four original attractors, while in the teb mutant scr could or could not be expressed either in the quiescent center or in the cortex-endodermis attractor.
it is worth noting that in both cases the basins of attraction changed.
for instance, consider the states that without any indetermination originally led to the cortex-endodermis attractor.
such states could now lead to vascular initials due to scr indeterminations, as expected given the experimental evidence.
it is also important to note that even though scr expression is clearly affected in real roots, cells may not switch among cell types.
however, the results derived from modeling the grn using antelope are consistent with data currently available and demonstrate the utility of this tool when we deal with networks in which the truth tables for some genes are not completely known.
figures  <dig> and  <dig> show screenshots of this analysis.
other properties
these two analyses were based on indeterminations, stable and unstable steady states, and basins of attraction of such states.
when designing and analyzing larger grns, more complex state attributes, such as global properties or conditional reachability may be useful.
for example, all the states occurring in either one-state or two-state attractors  satisfy the formula "↓σ.ex ex σ".
the formula "ef", in turn, can be used to calculate the basins of attraction of all such attractors.
hence, the formula "not)" would characterize the complement of all such basins of attraction.
this is equivalent to the set of all states in the basins of attraction of attractors with more than two states.
similarly, the set of states occurring in exactly two-state attractors can be calculated with the formula "↓σ.ex  and ex σ)".
these global properties cannot be expressed by ctl formulas.
conditional reachability can be expressed with the eu operator , a generalization of ef.
whereas "efs2" holds at all states from which it is possible to reach state s <dig>  "e" holds at all states from which it is possible to reach s <dig> by going only through states at which the formula φ holds.
for instance, the set of states from which it is possible to reach s <dig> without going through s <dig> corresponds to the formula "e".
by contrast, the set of states from which it is possible to reach s <dig> only by going through s <dig> at least once is the complement of the previous set of states with respect to the basin of attraction of s2: "not u s2]) and ef s2".
in formulas having such schemata, we would need to name states.
such a naming is possible in ctl by identifying a state with the conjunction of its nonnegated active genes and its negated inactive genes.
antelope, by contrast, provides more concise ways of referring to a state, with a number which, if written in binary, follows the lexicographic order of the names of the genes.
we refer the reader to the antelope user's manual and site.
discussion
other related systems
we now describe other systems relevant for us.
for brevity, we have to exclude certain works: first, we leave out boolean grn simulators, such as atalia  <cit> , booleannet  <cit> , and boolnet  <cit> .
second, we omit research based on structures other than kripke structures; examples are: a work utilizing the ltl  model checker of the maude system  <cit> , works using reactive modules with the mocha model checker  <cit> , and those employing probabilistic model checking with prism  <cit> .
we start with systems based on thomas' formalism and proceed with systems using continuous approaches.
gnbox
gnbox  <cit>  applies constraint logic programming techniques  <cit>  to thomas' formalism  <cit> .
such a formalism establishes a search space resulting from states possibly having more than one successor.
a straightforward implementation of a logic programming language  typically traverses a search space following a depth-first, top-down discipline in the same way as an ordinary simulator.
unlike a simulator employing a random device, however, such an implementation utilizes backtracking.
observe that a depth-first, top-down discipline together with backtracking can take an exponential amount of time in the size of the model .
constraint logic programming languages, nevertheless, use constraints to efficiently traverse the search space.
in particular, gnbox expresses constraints as a boolean satisfiability  problem that is turned over to a dedicated sat solver.
this approach is able to model many possible grns, thereby pruning the search space and eliminating the need for performing numerous simulations.
by expressing desired properties as constraints, gnbox can find parameter values of grns represented in thomas' framework.
ginsim
ginsim  <cit>  also uses a variant of thomas' formalism.
as in such a formalism, networks in ginsim have indeterminations representing asynchrony.
ginsim computes the state transition graph of the grn  before proceeding to analyze a trajectory selected by the user.
ginsim can also classify circuits in the interaction diagram  and can compute the set of all  steady states of grns which do not have indeterminations using mdds, a multi-value generalization of bdds.
finally, ginsim can find the strongly connected components of the state-transition graph or the interaction graph.
smbionet and mateus et al.
's system
smbionet  <cit>  employs a variant of thomas' formalism as well.
the input is an interaction diagram of the grn under study, together with desired properties expressed as ctl formulas.
the output is a set of all the models conforming to the given interaction diagram and which also satisfy the given formulas.
candidate models are generated by instantiating parameters and then tested with a model checker.
another system also using both thomas' formalism and temporal logic is that by mateus et al.
<cit> .
inequalities over the parameters of the model are obtained from the interaction diagram.
these inequalities are augmented with ltl formulas specifying desirable properties of the model.
the model is traversed forward and paths that do not satisfy the constraints are eliminated, so that only paths satisfying the constraints are retained.
squad
squad  <cit>  combines a continuous model, employing ordinary differential equations, with a boolean model of the network.
the user provides the interaction diagram of the network, from which squad obtains a continuous model.
to find steady states of the continuous model, squad first converts such a model into an approximate boolean asynchronous model.
in the boolean model, squad then computes, using bdds and a random device, the set of states probably belonging to attractors of any size and occurring in attractors without indeterminations .
next, squad repetitively uses such states as initial states in a continuous simulator to search for steady states in the continuous model.
perturbations may be introduced to confirm that such steady states are stable and to identify the effect of specific genes.
gna
gna  <cit>  is based on piecewise-linear differential equations.
unlike other systems using this formalism, the user need not specify precise values of parameters.
instead, less precise intervals are employed.
states are qualitative and represent ranges of concentrations of proteins, so that simulations are also qualitative.
in addition, gna computes a discrete abstraction  <cit>  of the continuous model, that can be verified with standard model checkers .
the user in this case can express simple properties in ctl.
for more complex properties, the gna group has developed its own logic, called computation tree regular logic  <cit> .
this logic extends ctl with regular expressions and fairness operators, allowing the expression of properties such as multistability and oscillations.
finally, gna has a formula editor, guiding the user in writing new formulas.
biocham
biocham  <cit>  can analyze and simulate biochemical networks using boolean, kinetic, and stochastic models.
in addition, properties can be formalized in temporal logic , so that a model checker can be used to validate such properties.
biocham models a network of protein interactions as a set of biochemical reaction rules, such as a+b = > c. indeterminations appear because such a rule, for instance, is translated into four transitions going out of the same state, resulting from the four combinations of either reactant a or reactant b being completely or incompletely consumed.
in addition, biocham has a model-update module, repairing models that do not satisfy the formalized properties.
comparison and planned features
on the one hand, compared with systems employing constraints, antelope, by using bdds, can compute large sets of states having a certain ctl property .
on the other hand, compared with simulators, in addition to this benefit, antelope can prove assertions about infinitely many paths, as opposed to only drawing statistical conclusions.
it is interesting to observe, though, that some systems built around a simulator  leave the simulation technique for bdds when calculating steady states .
we also find differences between antelope and other systems using model checking.
for instance, smbionet, mateus et al.
's system, gna, and biocham perform model checking for verification, using a model checker to confirm or deny that a certain formula is satisfied.
antelope, by comparison, employs model checking for calculating sets of states.
a first clear limitation of antelope when compared with systems based on thomas' formalism  is its being restricted to boolean genes.
we thus plan to extend antelope with multi-valued genes.
in this case, it would be interesting to try to incorporate into antelope techniques using constraints, like those of gnbox, for determining parameter values.
currently, antelope's grns are only either completely synchronous or completely asynchronous.
another improvement would then be the possibility of representing partially asynchronous grns, as employed in  <cit> .
many of the systems we reviewed allow the user to draw the grn, whereas currently antelope only accepts textual formats for describing the grn.
clearly, future versions of antelope should also have such drawing capabilities.
in addition, gna, for instance, has a formula editor, which would be desirable in antelope as well.
by contrast, antelope is a web application, requiring no installation of any local software from the user other than a standard web browser.
moreover, antelope can also run locally, exhibiting advantages of both web and local applications.
we can mention two further additions requiring more substantial work.
biocham has an update module, repairing faulty models.
a similar update module would also enhance antelope's features.
another improvement, as with any model checker, would be the addition of more powerful methods for approaching the state-explosion problem.
currently, antelope only has bdds for representing large sets of states, but new techniques, such as cegar   <cit>  would enable antelope to deal with larger grns.
CONCLUSIONS
systems for analyzing and building boolean grns employ branching time almost exclusively for representing asynchronous transitions.
thomas' work, however, represents two other important phenomena with branching time, namely incomplete specifications and environment interaction.
a consequence of including these two other kinds of indetermination is that unstable steady states may appear.
we have shown how having both stable and unstable steady states is useful for developing boolean grns.
in addition, we reviewed and extended the advantages of model checking, as compared with simulation, in the presence of indeterminations.
in particular, we observed that model checkers, unlike simulators randomly selecting a successor, can prove properties of a set of infinitely many paths.
another advantage we reviewed is that of handling new, unforeseen properties: while model checkers can often represent new properties with additional temporal-logic formulas, simulators require the incorporation of such properties in their program code.
we illustrated the advantages of two extensions to ordinary model checking.
first, we noted that ordinary model checkers would only confirm or deny that all the states in a given set of states have a certain property.
by contrast, we claimed that model checkers are more useful for reasoning about boolean grn when exhibiting the set of states that have a property of interest.
second, we observed that the logics  underlying many model checkers are not expressive enough for representing many interesting properties of boolean grns.
antelope tries to overcome these two limitations by showing the set of states satisfying a given formula, and by employing a hybrid extension of ctl.
it is important to remark that model checkers for hybrid logics are both relevant and neglected.
as pointed out in  <cit> , "the implementation of model checkers for hybrid logics still remains a quite unexplored field of research".
other than antelope, we only know of two hybrid model checkers  <cit> .
these, however, employ a basic modal logic instead of ctl, and their implementations do not use bdds.
this makes antelope the first symbolic model checker for hybrid ctl  with which to experiment in the development of boolean grns.
availability and requirements
•project name: antelope
•project home page: http://turing.iimas.unam.mx:8080/antelopeweb/
•operating system: platform independent
•programming language: java
•other requirements: any standard web browser
•license: gpl
•any restrictions to use by non-academics: none other than those in gpl
authors' contributions
ga did most of the web interface.
ja participated in the design of, and wrote the code for, the previous version of antelope's model checker.
ea contributed to the design of the stem cell niche grn from the literature data, used antelope, and participated in writing the biology part of this paper, as well as the manual.
mb also contributed to the design of the stem cell niche grn from the literature data and wrote the rest of the biology part of this paper, as well as the manual.
mc suggested using hybrid ctl to overcome ctl limitations, participated in the design of antelope, contributed to the presentation of these results, and wrote the formal definitions of ctl and hybrid ctl .
pg wrote the code for antelope's model checker, connected the model checker with the web interface, embedded antelope and apache tomcat in a single file, did the rest of the web interface, and added numerous features to antelope.
dar participated in the design of antelope and wrote the model-checking part of this paper.
erab put forward the idea of testing kauffman's hypothesis that boolean grns can recover experimental gene expression profiles, and led the translation of actual data into the the stem cell niche grn.
all authors read and approved the final manuscript.
supplementary material
additional file 1
a gentle introduction to  computation-tree logic.
this additional file has gentle introductions to computation-tree logic and hybrid computation-tree logic.
click here for file
additional file 2
computation-tree logic.
this additional file has formal definitions of computation-tree logic and hybrid computation-tree logic.
click here for file
additional file 3
benchmarks.
this additional file shows the execution time for several examples.
click here for file
additional file 4
antelope user's manual.
this additional file has the antelope user's manual.
click here for file
acknowledgments
this paper owes much to pablo padilla-longoria, who carefully read a previous version of this paper and subsequently had valuable discussions with us.
we also thank carlos velarde, who patiently helped us with latex, montserrat alvarado, who helped us translating the first version of antelope's manual and generating the figures, and who is in charge of turing.iimas.unam.mx, gabriel muñoz-carrillo and jorge hernández, who helped us translating the first version of antelope's windows and menus, carlos gershenson and nathan weinstein, who gave us useful suggestions, and michael dent and michael scott white, who proposed english changes.
we gratefully acknowledge the facilities provided by the iimas, the instituto de ecología, and the centro de ciencias de la complejidad.
mb participated in this paper through the centro de ciencias de la complejidad, by means of the "red de conacyt complejidad, ciencia y sociedad".
mb was also supported by the czech ministry of education, youth and sports .
erab acknowledges the financial support from conacyt grants  <dig>   <dig>  and  <dig>  and papiit grants in <dig>  in229009- <dig>  and in223607- <dig>  dar acknowledges the financial support from papiit grant in120509- <dig>  finally, we are grateful to the referees whose comments helped improve the previous version of this paper.

 gene regulatory network models a major challenge in current biology is relating spatio-temporal gene expression patterns to phenotypic traits of an organism. these patterns result partly from complex regulatory interactions sustained principally by genes and encoded proteins. the complexity of such interactions exceeds the human capacity for analysis. thus, mathematical and computational models of gene regulatory networks are indispensable tools for tackling the problem of mapping the genotype into the phenotype. these models have been fruitfully applied in numerous biological systems. within the various kinds of grn models, boolean grns are especially valuable for their simplicity and for nonetheless having a rich behavior yielding meaningful biological information. examples where boolean grns have been successfully used are: the segment polarity gene network of drosophila melanogaster, the flower organ determination grn of arabidopsis thaliana, the mammalian cell cycle, and the yeast cell cycle. in a boolean grn, each gene has only two possible activation values: active or inactive; intermediate expression levels are neglected. a network state at time t is a vector containing the activation values of all the genes in the grn at time t. in addition, time is viewed as proceeding in discrete steps. the value of every gene x at time t + is specified by a boolean function of the values of its regulators g g …,gnx at time t. branching time boolean grns are closely related to the formalism developed by thomas and his collaborators. thus, computer systems for boolean grns are often influenced by thomas' formalism, which employs grn models with branching time, allowing states with more than one immediate future. a network state with more than one immediate future represents the fact that the next state of the regulatory system modeled by such a grn can be any one of several states. hence, the next state of the modeled system is only partially determined. let us then say that there is an indetermination in the network. this indetermination in the system's behavior reflects a certain degree of unpredictability that can be identified with several important phenomena. asynchrony one such phenomenon is asynchrony. experiments for inferring gene interaction do not normally establish the length of time between state changes. hence, when such experiments indicate the change in value of two genes, say, it is preferable to model such a situation with a single state having two successors, one for each change, as illustrated in figure the reasons are that we do not know the relative values of both delays in real biological systems and that complete synchrony might be practically impossible. many computer systems based on, or inspired by, thomas' formalism employ asynchronous models. thomas' formalism, however, incorporates two additional phenomena with indeterminations, that are typically excluded in such systems. incompletely specified behavior one such additional phenomenon is incompletely specified behavior. this behavior may emerge, first, from a "synthetic" approach, where we are interested in all boolean grns having certain properties regardless of other properties. the tables specifying the network behavior would then have outputs whose value "does not matter". second, lack of some of the experimental information of a regulatory system also emerges as incompletely specified behavior. in this case, the behavior tables would have outputs whose value we do not know. interaction with the environment another phenomenon usually neglected in computer systems for grn analysis and that can be modeled with branching time is that of interaction with the environment. assume that the next state of a regulatory system depends on the temperature: if the temperature is low, the system's next state will be one, but if the temperature is high, the system's next state will be different. another example is the unpredictability of radiation-induced apoptosis. in this case, for the same degree of radiation some cells will initiate apoptosis while others will not. thomas and d'ari reflect such an unpredictability with an "input variable" of an unknown value. this phenomenon can be readily incorporated with indeterminations. simulators boolean grns are sometimes studied with simulators. a simulator attempts to replicate the behavior of a system by performing state changes in the same order as they occur in the system being modeled. hence, network paths are traversed forward from one state to the next. in the presence of a state with more than one successor, such a straightforward approach must be complemented with additional mechanisms. two of such mechanisms are: a random device and backtracking coupled with a cycle-detection mechanism. a random device, on the one hand, allows for only drawing statistical conclusions. the reason is that in the presence of a state with more than one successor, the number of paths may be infinite, as depicted in figure backtracking and cycle detection, on the other hand, can be inefficient. there are two important approaches for circumventing these difficulties. one of these techniques is an elaboration of backtracking so as to increase its efficiency by requiring certain constraints to be satisfied as the network is traversed. the work by corblin et al. uses this approach. another relevant method is model checking. model checking model checking is a collection of techniques for automatically verifying properties especially of discrete systems. the main ideas of model checking appeared years ago. at present, numerous model-checking tools exist. model checking is routinely used, mainly for hardware verification, but also for software verification, and was distinguished with the a. m. turing award in model checking has been advocated for analyzing biological systems with increasing interest. a model checker normally has as input a "kripke structure" representing a discrete system, a distinguished "initial" state in the kripke structure, and a "temporal-logic" formula expressing a desirable property, that may or may not hold at a state. the output of the model checker is either a confirmation or a denial that the formula holds at the initial state. in a kripke structure time is branching, so that there may be more than one possible future of a given state. the introduction of branching time may produce infinitely many forward traversals. model checkers, however, unlike simulators randomly selecting a successor state, can systematically analyze such infinitely many possibilities. intuitively, this is often done by traversing the kripke structure in reverse and accumulating the set of all states at which a subformula holds. model checking amounts, thus, to performing an exhaustive search. such a search plays the role of a mathematical proof establishing a property for infinitely many paths. programming vs. formula writing by being based on properties formalized in temporal logic, model checkers have another advantage over simulators. the decision of whether or not a state satisfies a property of interest is programmed in the simulator itself. therefore, if an unforeseen property appears during the usage of a boolean grn simulator, such a property must be incorporated in the simulator by modifying program code. this renders simulators rigid: either the user's needs are anticipated or reprogramming must be done. compared with simulators, model checkers exhibit the benefit of having replaced programming with temporal-logic formula writing. instead of having to modify the computer program of a simulator, many new queries can be dealt with by writing new temporal-logic formulas, which are concise and self-contained. organization of this paper in the implementation section, we first illustrate both computation-tree logic and its hybrid extension, hybrid ctl, chosen to be able to express interesting properties for boolean grn analysis and construction. the term "hybrid" here means a combination of propositional modal logic with classical predicate logic, and should not to be confused with hybrid model checking, combining discrete with continuous variables. the implementation section subsequently covers the model-checking algorithms and some implementation details. next we show, in the results section, the use of the antelope model checker in the presence of indeterminations either caused by environment interaction or by an incompletely specified behavior. finally, the discussion section reviews other similar software systems, compares antelope with such systems, and outlines features planned for the future. implementation this section first covers the temporal logics used by antelope. after explaining ctl, we turn our attention to its hybrid extension. next, we cover the model-checking algorithms, as well as additional implementation issues. computation-tree logic we now give a short account of ctl and refer the reader to additional file of this paper for a gentle introduction and to additional file for a formal definition of ctl. more thorough treatments can be found in. boolean and temporal operators formulas in ctl can have boolean operators, such as not and or. in addition, such formulas can have "temporal operators", allowing us to refer to formulas holding in the future of a particular state. in this case, we must indicate whether we mean some future or all futures. hence, it is possible to refer either to some path starting in the present with the "modality" e, or to all paths starting in the present with the modality a. similarly, it is possible to refer to the immediate future with the modality x, to any state in the present or any point in the future with the modality f, or to all states in the present and in the future with the modality g. table summarizes these modalities. a temporal operator is composed of a modality in the upper part together with a modality in the lower part of this table, which results in six temporal operators. for example, a formula asserting that there exists a path such that in the present or in the future g does not hold and g does hold would be: "ef and g1)". hence, assuming that there is a single state s in which g does not hold and g does hold, this formula can be used to obtain the basin of attraction of such a state, with a model checker computing all states at which a given formula holds. the formula "ax and g1)" holds at all states from which it is necessary to reach s in one step, i.e., states which have s as their only next state. the formula "ex and g1)" holds at all states from which it is possible to reach s in one step, i.e., states which have s as a next state. other ctl formulas can characterize, for instance, whether or not it is necessary to go through a state s to reach another state s see for a list of ctl formulas specifying various biological properties. some properties not expressible in ctl there do not exist, however, ctl formulas for characterizing steady states, or oscillations. this motivates the use of a more expressive logic than ctl. antelope provides a "hybrid" extension of ctl. hybrid computation-tree logic this subsection is devoted to hybrid ctl. we refer the reader to additional file of this paper for a gentle introduction and to additional file for a formal definition of hybrid ctl. deeper treatments of hybrid logics are in. state variables the main idea behind the hybrid extension of a temporal logic consists in the addition of variables allowing us to refer to states. the downarrow binder "↓σ" sets the state variable σ to the current state of evaluation. the formula "↓σ.ax σ", for example, characterizes the set of states which have themselves as their only next state. hence, hybrid ctl allows us to characterize the set of steady states. moreover, by employing branching time, we are able to distinguish between two kinds of steady state. when a state has only one transition from and to itself, following thomas and d'ari, we will call it a stable steady state. when a state has, in addition to a self-loop, other transitions going to other states, following, we will call it an unstable steady state. hybrid ctl formulas for calculating both these sets of states are: "↓σ.ax σ", for the set of stable steady states, and "↓σ.exσ", for the union of the sets of stable and unstable steady states. other formulas attractors of various sizes and oscillations the notion of a steady state can be generalized in an attractor, possibly involving more than one state. a steady state would then be a one-state attractor. a formula characterizing attractors of any size would be: "↓σ.ex ef σ". another interesting formula would be "↓σ.ex and ex σ)", which holds at states belonging to a size-two attractor. oscillations, where a gene is alternatively active and inactive, can also be characterized in hybrid ctl: additional file explains a formula for the basin of attraction of possible oscillations. we refer the reader to the antelope web site http://turing.iimas.unam.mx:8080/antelopeweb/ for more formulas. algorithms ctl antelope uses a standard "labeling" algorithm for ordinary ctl formulas. labeling algorithms for model checking are so called because we can think of each state as being labeled with the subformulas holding at that state. say that the formula given by the user is φ. the labeling algorithm starts by considering the simplest subformulas of φ, that is, the names of the genes. for each gene g, labeling all states at which the formula "g" holds is easy, as that information is already present in the kripke structure. next, the labeling algorithm proceeds to more complex subformulas, until φ is reached, by treating the operator of each such subformula by cases. for instance, if the subformula is of the form "ψ and ψ2", then the labeling algorithm computes the set of states at which such a subformula holds as the intersection of the set of states at which ψ holds with the set of states at which ψ holds. all boolean operators can be treated by combining set operations, like union, intersection, and set difference. the labeling algorithm treats some temporal operators, such as ax, by using equivalences. for example, "ax ψ" is equivalent to "not ex not ψ". the rest of the temporal operators, however, must be dealt with explicitly. for all such primitive operators the labeling algorithm traverses the kripke structure in reverse. take for instance "ex ψ", which holds if there exists a next state at which ψ holds. given the set of states at which ψ holds, the labeling algorithm treats "ex ψ" by obtaining all states which have an immediate successor in such a set, i.e., all the predecessors of the states in such a set. the labeling algorithm processes operators such as eg by repetitively traversing the kripke structure in reverse. hybrid ctl the labeling algorithm is efficient. the additional expressiveness of hybrid operators, such as "↓" comes at a price, however. given a ctl formula φ, the computation of the set of states at which a formula of the form "↓σ.φ" holds involves calling the labeling algorithm with φ once for each state. the decrease in efficiency is even more if the "↓" operator appears nested. antelope, however, treats certain patterns in special ways, requiring less time than a direct approach. more implementation issues antelope is a symbolic model checker, representing state sets by reduced, ordered binary-decision diagrams. representation of a set of states a bdd is a representation of a boolean function. thus, to use a bdd for representing a set of states in a kripke structure we must view such a set as a boolean function. this is possible if each row of the truth table of the boolean function corresponds to an element which may or may not belong to such a set. the value of such a function will be at exactly those states belonging to the set. representation of a set of transitions in addition to representing sets of states, bdds are used for representing the set of transitions of kripke structures. in this case, the boolean function has twice as many variables as there are genes. the reason is that each transition has both a source and a terminating state. bdds are often surprisingly concise, allowing the verification of many large kripke structures, with more than states. we refer the reader to for a detailed description of bdds and their use in symbolic model checking. optimizations apart from the use of bdds, antelope has several "optimizations". for example, a straightforward formula characterizing the states with more than one successor has the pattern "↓σ.ex ↓τ.φ". if evaluated as described in the algorithms section, this formula would call the labeling algorithm a number of times proportional to the square of the number of states, where |s| is the number of states). to find the set of states with more than one successor, however, it is not necessary to visit all states for each state of the kripke structure. it suffices to be able to enumerate the successors of each state. antelope treats the formula for characterizing the states with more than one successor as a special case so that the ctl model-checking algorithm is called with φ as input a number of times linear in the size of the kripke structure, where |r| is the number of transitions). another optimization is that of the operator ey, which is the converse of ex. although this operator need not be primitive, antelope does treat it as primitive by simply traversing the transitions forward. this operator allows the user to view antelope as a kind of simulator. additional file has a table comparing the verification times for a few models with respect to some properties of increasing complexity. input formats antelope accepts two formats for describing the boolean grn: tables and equations. in both cases, the values of a gene are specified as a boolean relation which depends on the values of genes. a table can be viewed as an extension of an ordinary truth table, where stars are allowed on the right-hand side, denoting indeterminations. sometimes, however, it may be more convenient to use a logical formula instead of a truth table. hence, antelope accepts equations, each of which is of the form: x:=fx where the left-hand side represents the value of the gene x at the current time step, and the right-hand side is an arbitrary boolean function on the values of genes at the previous time step. to be able to represent indeterminations, we need two equations with the same left-hand side. we refer the reader to the antelope user's manual, which appears in additional file and in the url http://turing.iimas.unam.mx:8080/antelopeweb/.  we now exemplify the use of antelope for analyzing boolean variants of the a. thaliana root stem cell niche grn. stem cells or initials are undifferentiated cells from which particular cell types of the organisms are generated; the microenvironment in which stem cells are located is called the stem cell niche. anatomically, stem cell niches are conformed by two different cell types, the stem cells themselves, and another cell or group of cells sometimes generically called organizer cells. the organizer cells maintain the stem cells in the undifferentiated state through short-range signals. understanding how the different cells conforming stem cell niches are specified, as well as how the balance between cell division and cell differentiation is maintained in the niches, is central for understanding the development, growth and regeneration processes occurring in plants and animals. in particular, plant stem cell niches constitute valuable model systems for studying regenerative and plastic developmental processes, as these organisms grow new organs and structures throughout their life. we focus on the root stem cell niche of a. thaliana, that is located near the root tip and is well characterized at the anatomical and molecular level. this niche is conformed by the so-called quiescent center, which is in turn conformed by the organizer cells of the root scn, and is surrounded by four different stem cell types. each of these four types of stem cell will give rise to a different cell lineage: vascular, cortex/endodermal, epidermal, and columella/root-cap cells. however, in this contribution two of the stem cell types are considered as only one since the available experimental evidence is not enough to distinguish between them at the gene expression level, leaving only four types of initial cells, and epidermal/root-cap initials). besides being thoroughly characterized at the anatomical level, the root stem cell niche of a. thaliana has been relatively well described from a molecular and genetic perspective. indeed, some of the molecular components that are necessary to establish and maintain the root scn cellular patterning have been recently uncovered. among these components are the genes short-root and its target gene scarecrow, the immediately downstream genes of the dimer shr/scr, and other genes that interact with them. another set of relevant genes includes the plethora genes, which have been proposed to be key components of the molecular readout of the plant hormone auxin. finally, the qc specific gene wuschel related homeobox is fundamental for root scn organization; see the graphical representation of the interactions between these genes in figure moreover, the expression patterns of these genes and the localization of their corresponding proteins have been described. thus, it is possible to postulate a gene expression profile that characterizes each of the scn cell types mentioned above according to the table in order to define the rules for a boolean grn model for this system, we considered all the genes that have been reported to play a relevant role in the specification of the root stem cells and gathered the available experimental information for the regulation of their expression; see figure these data included mostly molecular genetics experiments, such as experiments with plants containing a mutant allele of a gene. the resulting rules can be summarized in the following logical statements: // shr; without regulators // auxin; without regulators plt: = arf; auxins: = auxins; iaa: = ~ auxins; arf: = ~ iaa; shr: = shr; scr: = shr & scr &; jkd: = shr & scr; mgp: = shr & scr &~ wox; wox: = arf & shr & scr &; as has been proposed for other systems, we expected the stable steady states of our grn model to correspond to the gene expression profiles characterizing the different stem cells within the root niche of a. thaliana. thus, from our knowledge of the system, we expected four stable steady states. the expected steady states are indeed obtained after postulating a mutual negative interaction between wox and mgp, which gives rise to a new testable prediction. using this grn model, we first illustrate the use of indeterminations representing incomplete experimental data. next, we use indeterminations for modeling the influence of unpredictable external signals. experimental gap steady states and scarecrow while developing the truth tables for this grn, we detected an experimental gap. we know that scarecrow, a target gene of the dimer shortroot /scr, either loses or diminishes its own expression in the jackdaw single mutant in the stem cell niche. the same is true for scr-dependent quiescent-center marker qc. the magpie mutant, by contrast, has no visible phenotype. finally, the mgp jkd double mutant recovers the scr expression. based on this information, we established the truth table for scr, which appears in table observe the indetermination, reflecting the fact that activity could or could not be lost in a jkd background. antelope produced three stable steady states, but four unstable steady states. hence, removing the indetermination in the above table may recover the four expected stable steady states. we performed the jkd loss-of-function simulation in our models to distinguish which of the two possibilities recovered the expected states. interestingly, following the grn state transitions backwards, using the ex operator, we noted that if scr is unable to be expressed in jkd, then neither the wuschel-related homebox expression nor the scr expression disappeared at the quiescent-center. furthermore, our jkd mutant does cause a loss of the cortex-endodermis initials attractor, contrary to what is observed in experimental jkd mutants, suggesting that jkd only diminishes scr expression. again, following the grn transitions backwards for the case in which jkd loss-of-function does not lose scr expression, we found that the system was able to recover the jkd loss-of-function mutant. based on the result found with the system including indeterminations, we replaced the star by a in the table for scr. once the indetermination was so removed, we obtained four stable steady states. external signals fas and scr let us now exemplify antelope as used for modeling the effect of external signals that affect one or more grn nodes. the root stem cell niche of a. thaliana is affected by several external signals, such as genes and molecules from modules involved in other processes in the organism. for example, kaya and collaborators reported that fasciata and fasciata, hereafter collectively called fas, affect scr expression. in the fas mutant, scr expression is deregulated and can be either expressed or not expressed in almost any cell of the root stem cell niche. similarly, inagaki and collaborators reported the techbi mutants also affecting scr expression. again, when teb is mutated, scr may or may not be expressed through the endodermal layer, the cortex-endodermis initial cells, and the quiescent center. we incorporated fas by adding a variable fas to the truth table for scr. for fas = the truth table obtained in the "experimental gap" subsection was used. for fas = by contrast, all the right-hand sides of the new truth table had indeterminations. in the case of teb, we only used indeterminations for the right-hand side of the scr table where the output was for the teb mutant. we found that under these conditions the original four attractors were preserved in both cases. we also found that in the fas mutant, scr could be expressed in any of the four original attractors, while in the teb mutant scr could or could not be expressed either in the quiescent center or in the cortex-endodermis attractor. it is worth noting that in both cases the basins of attraction changed. for instance, consider the states that without any indetermination originally led to the cortex-endodermis attractor. such states could now lead to vascular initials due to scr indeterminations, as expected given the experimental evidence. it is also important to note that even though scr expression is clearly affected in real roots, cells may not switch among cell types. however, the results derived from modeling the grn using antelope are consistent with data currently available and demonstrate the utility of this tool when we deal with networks in which the truth tables for some genes are not completely known. figures and show screenshots of this analysis. other properties these two analyses were based on indeterminations, stable and unstable steady states, and basins of attraction of such states. when designing and analyzing larger grns, more complex state attributes, such as global properties or conditional reachability may be useful. for example, all the states occurring in either one-state or two-state attractors satisfy the formula "↓σ.ex ex σ". the formula "ef", in turn, can be used to calculate the basins of attraction of all such attractors. hence, the formula "not)" would characterize the complement of all such basins of attraction. this is equivalent to the set of all states in the basins of attraction of attractors with more than two states. similarly, the set of states occurring in exactly two-state attractors can be calculated with the formula "↓σ.ex and ex σ)". these global properties cannot be expressed by ctl formulas. conditional reachability can be expressed with the eu operator, a generalization of ef. whereas "efs2" holds at all states from which it is possible to reach state s "e" holds at all states from which it is possible to reach s by going only through states at which the formula φ holds. for instance, the set of states from which it is possible to reach s without going through s corresponds to the formula "e". by contrast, the set of states from which it is possible to reach s only by going through s at least once is the complement of the previous set of states with respect to the basin of attraction of s2: "not u s2]) and ef s2". in formulas having such schemata, we would need to name states. such a naming is possible in ctl by identifying a state with the conjunction of its nonnegated active genes and its negated inactive genes. antelope, by contrast, provides more concise ways of referring to a state, with a number which, if written in binary, follows the lexicographic order of the names of the genes. we refer the reader to the antelope user's manual and site. discussion other related systems we now describe other systems relevant for us. for brevity, we have to exclude certain works: first, we leave out boolean grn simulators, such as atalia, booleannet, and boolnet. second, we omit research based on structures other than kripke structures; examples are: a work utilizing the ltl model checker of the maude system, works using reactive modules with the mocha model checker, and those employing probabilistic model checking with prism. we start with systems based on thomas' formalism and proceed with systems using continuous approaches. gnbox gnbox applies constraint logic programming techniques to thomas' formalism. such a formalism establishes a search space resulting from states possibly having more than one successor. a straightforward implementation of a logic programming language typically traverses a search space following a depth-first, top-down discipline in the same way as an ordinary simulator. unlike a simulator employing a random device, however, such an implementation utilizes backtracking. observe that a depth-first, top-down discipline together with backtracking can take an exponential amount of time in the size of the model. constraint logic programming languages, nevertheless, use constraints to efficiently traverse the search space. in particular, gnbox expresses constraints as a boolean satisfiability problem that is turned over to a dedicated sat solver. this approach is able to model many possible grns, thereby pruning the search space and eliminating the need for performing numerous simulations. by expressing desired properties as constraints, gnbox can find parameter values of grns represented in thomas' framework. ginsim ginsim also uses a variant of thomas' formalism. as in such a formalism, networks in ginsim have indeterminations representing asynchrony. ginsim computes the state transition graph of the grn before proceeding to analyze a trajectory selected by the user. ginsim can also classify circuits in the interaction diagram and can compute the set of all steady states of grns which do not have indeterminations using mdds, a multi-value generalization of bdds. finally, ginsim can find the strongly connected components of the state-transition graph or the interaction graph. smbionet and mateus et al.'s system smbionet employs a variant of thomas' formalism as well. the input is an interaction diagram of the grn under study, together with desired properties expressed as ctl formulas. the output is a set of all the models conforming to the given interaction diagram and which also satisfy the given formulas. candidate models are generated by instantiating parameters and then tested with a model checker. another system also using both thomas' formalism and temporal logic is that by mateus et al.. inequalities over the parameters of the model are obtained from the interaction diagram. these inequalities are augmented with ltl formulas specifying desirable properties of the model. the model is traversed forward and paths that do not satisfy the constraints are eliminated, so that only paths satisfying the constraints are retained. squad squad combines a continuous model, employing ordinary differential equations, with a boolean model of the network. the user provides the interaction diagram of the network, from which squad obtains a continuous model. to find steady states of the continuous model, squad first converts such a model into an approximate boolean asynchronous model. in the boolean model, squad then computes, using bdds and a random device, the set of states probably belonging to attractors of any size and occurring in attractors without indeterminations. next, squad repetitively uses such states as initial states in a continuous simulator to search for steady states in the continuous model. perturbations may be introduced to confirm that such steady states are stable and to identify the effect of specific genes. gna gna is based on piecewise-linear differential equations. unlike other systems using this formalism, the user need not specify precise values of parameters. instead, less precise intervals are employed. states are qualitative and represent ranges of concentrations of proteins, so that simulations are also qualitative. in addition, gna computes a discrete abstraction of the continuous model, that can be verified with standard model checkers. the user in this case can express simple properties in ctl. for more complex properties, the gna group has developed its own logic, called computation tree regular logic. this logic extends ctl with regular expressions and fairness operators, allowing the expression of properties such as multistability and oscillations. finally, gna has a formula editor, guiding the user in writing new formulas. biocham biocham can analyze and simulate biochemical networks using boolean, kinetic, and stochastic models. in addition, properties can be formalized in temporal logic, so that a model checker can be used to validate such properties. biocham models a network of protein interactions as a set of biochemical reaction rules, such as a+b = > c. indeterminations appear because such a rule, for instance, is translated into four transitions going out of the same state, resulting from the four combinations of either reactant a or reactant b being completely or incompletely consumed. in addition, biocham has a model-update module, repairing models that do not satisfy the formalized properties. comparison and planned features on the one hand, compared with systems employing constraints, antelope, by using bdds, can compute large sets of states having a certain ctl property. on the other hand, compared with simulators, in addition to this benefit, antelope can prove assertions about infinitely many paths, as opposed to only drawing statistical conclusions. it is interesting to observe, though, that some systems built around a simulator leave the simulation technique for bdds when calculating steady states. we also find differences between antelope and other systems using model checking. for instance, smbionet, mateus et al.'s system, gna, and biocham perform model checking for verification, using a model checker to confirm or deny that a certain formula is satisfied. antelope, by comparison, employs model checking for calculating sets of states. a first clear limitation of antelope when compared with systems based on thomas' formalism is its being restricted to boolean genes. we thus plan to extend antelope with multi-valued genes. in this case, it would be interesting to try to incorporate into antelope techniques using constraints, like those of gnbox, for determining parameter values. currently, antelope's grns are only either completely synchronous or completely asynchronous. another improvement would then be the possibility of representing partially asynchronous grns, as employed in. many of the systems we reviewed allow the user to draw the grn, whereas currently antelope only accepts textual formats for describing the grn. clearly, future versions of antelope should also have such drawing capabilities. in addition, gna, for instance, has a formula editor, which would be desirable in antelope as well. by contrast, antelope is a web application, requiring no installation of any local software from the user other than a standard web browser. moreover, antelope can also run locally, exhibiting advantages of both web and local applications. we can mention two further additions requiring more substantial work. biocham has an update module, repairing faulty models. a similar update module would also enhance antelope's features. another improvement, as with any model checker, would be the addition of more powerful methods for approaching the state-explosion problem. currently, antelope only has bdds for representing large sets of states, but new techniques, such as cegar would enable antelope to deal with larger grns.  systems for analyzing and building boolean grns employ branching time almost exclusively for representing asynchronous transitions. thomas' work, however, represents two other important phenomena with branching time, namely incomplete specifications and environment interaction. a consequence of including these two other kinds of indetermination is that unstable steady states may appear. we have shown how having both stable and unstable steady states is useful for developing boolean grns. in addition, we reviewed and extended the advantages of model checking, as compared with simulation, in the presence of indeterminations. in particular, we observed that model checkers, unlike simulators randomly selecting a successor, can prove properties of a set of infinitely many paths. another advantage we reviewed is that of handling new, unforeseen properties: while model checkers can often represent new properties with additional temporal-logic formulas, simulators require the incorporation of such properties in their program code. we illustrated the advantages of two extensions to ordinary model checking. first, we noted that ordinary model checkers would only confirm or deny that all the states in a given set of states have a certain property. by contrast, we claimed that model checkers are more useful for reasoning about boolean grn when exhibiting the set of states that have a property of interest. second, we observed that the logics underlying many model checkers are not expressive enough for representing many interesting properties of boolean grns. antelope tries to overcome these two limitations by showing the set of states satisfying a given formula, and by employing a hybrid extension of ctl. it is important to remark that model checkers for hybrid logics are both relevant and neglected. as pointed out in, "the implementation of model checkers for hybrid logics still remains a quite unexplored field of research". other than antelope, we only know of two hybrid model checkers. these, however, employ a basic modal logic instead of ctl, and their implementations do not use bdds. this makes antelope the first symbolic model checker for hybrid ctl with which to experiment in the development of boolean grns. availability and requirements •project name: antelope •project home page: http://turing.iimas.unam.mx:8080/antelopeweb/ •operating system: platform independent •programming language: java •other requirements: any standard web browser •license: gpl •any restrictions to use by non-academics: none other than those in gpl authors' contributions ga did most of the web interface. ja participated in the design of, and wrote the code for, the previous version of antelope's model checker. ea contributed to the design of the stem cell niche grn from the literature data, used antelope, and participated in writing the biology part of this paper, as well as the manual. mb also contributed to the design of the stem cell niche grn from the literature data and wrote the rest of the biology part of this paper, as well as the manual. mc suggested using hybrid ctl to overcome ctl limitations, participated in the design of antelope, contributed to the presentation of these results, and wrote the formal definitions of ctl and hybrid ctl. pg wrote the code for antelope's model checker, connected the model checker with the web interface, embedded antelope and apache tomcat in a single file, did the rest of the web interface, and added numerous features to antelope. dar participated in the design of antelope and wrote the model-checking part of this paper. erab put forward the idea of testing kauffman's hypothesis that boolean grns can recover experimental gene expression profiles, and led the translation of actual data into the the stem cell niche grn. all authors read and approved the final manuscript. supplementary material additional file 1 a gentle introduction to computation-tree logic. this additional file has gentle introductions to computation-tree logic and hybrid computation-tree logic. click here for file additional file 2 computation-tree logic. this additional file has formal definitions of computation-tree logic and hybrid computation-tree logic. click here for file additional file 3 benchmarks. this additional file shows the execution time for several examples. click here for file additional file 4 antelope user's manual. this additional file has the antelope user's manual. click here for file acknowledgments this paper owes much to pablo padilla-longoria, who carefully read a previous version of this paper and subsequently had valuable discussions with us. we also thank carlos velarde, who patiently helped us with latex, montserrat alvarado, who helped us translating the first version of antelope's manual and generating the figures, and who is in charge of turing.iimas.unam.mx, gabriel muñoz-carrillo and jorge hernández, who helped us translating the first version of antelope's windows and menus, carlos gershenson and nathan weinstein, who gave us useful suggestions, and michael dent and michael scott white, who proposed english changes. we gratefully acknowledge the facilities provided by the iimas, the instituto de ecología, and the centro de ciencias de la complejidad. mb participated in this paper through the centro de ciencias de la complejidad, by means of the "red de conacyt complejidad, ciencia y sociedad". mb was also supported by the czech ministry of education, youth and sports. erab acknowledges the financial support from conacyt grants and and papiit grants in in229009- and in223607- dar acknowledges the financial support from papiit grant in120509- finally, we are grateful to the referees whose comments helped improve the previous version of this paper.
first, ordinary model checkers normally only verify whether or not a given set of model states has a given property. 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 cannot. second, for efficiency, the expressiveness of many model checkers is limited, resulting in the inability to express some interesting properties of boolean grns. we have developed antelope, a model checker for analyzing and constructing boolean grns. currently, software systems for boolean grns use branching time almost exclusively for asynchrony. 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. in comparison, a model checker for boolean grns is preferable if it reports the set of states having a desired property. we illustrate the advantages of antelope when modeling incomplete networks and environment interaction, exhibiting the set of all states having a given property, and representing boolean grn properties with hybrid ctl. 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. by representing a certain degree of unpredictability, branching time can model several important phenomena, such as asynchrony, incompletely specified behavior, and interaction with the environment. this additional expressiveness is achieved by employing a logic extending the standard computation-tree logic with hybrid-logic operators. model checkers for branching time, by contrast, are able to prove properties in the presence of infinitely many paths. antelope, by contrast, also uses branching time for incompletely specified behavior and environment interaction. in thomas' formalism for modeling gene regulatory networks, branching time, where a state can have more than one possible future, plays a prominent role.
 in thomas' formalism for modeling gene regulatory networks, 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 asynchrony, incompletely specified behavior, and 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, 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 cannot. this additional expressiveness is achieved by employing a logic extending the standard computation-tree logic with hybrid-logic operators.  we illustrate the advantages of antelope when modeling incomplete networks and environment interaction, exhibiting the set of all states having a given property, and representing boolean grn properties with hybrid ctl. 