Many of the Boolean networks from the literature are threshold networks 
. Each node can have a 0 or 1 value, and the value of a node when it is next updated is one if the sum of positive inputs minus the of negative inputs exceeds a constant threshold for that node. In analyzing and modifying these models, we found it to be necessary to extend threshold networks to handle more than two values.
levels of activation,
represents a functionally inactive level and
represents maximum activity. Three levels were sufficient for all of the networks appearing here. Each node has a specified threshold between each successive activation level, and each node input has an associated real-valued weight representing the strength of the reaction on the node.
Formally, a Boolean network is defined to have a set of
nodes associated with proteins. Each node has a set of inputs, which are other nodes. Each input also has an input weight
. In the networks here, only three magnitudes of weights are required:
. Inputs with positive weights are activating
and inputs with negative weights are inhibiting
. Each node
. The weighted sum of the inputs to a node are compared with these thresholds to determine whether the node level is enabled to increase or decrease. In the networks here,
for all nodes.
The network can be depicted as a directed graph. Nodes are labeled circles, and lines with arrowheads (for activating inputs) or flat ends (for inhibiting inputs) represent the inputs to nodes. The thickness of the line represents the weight on that input.
The dynamics of a network are represented as a Kripke structure
, which is a directed graph of states
, where each state consists of an assignment of a value of
to each node in the network. The Kripke structure has edges from each state to one or more successor states
; these edges represent possible ways that the states can change over time. The Kripke structure is deterministic
if each state has exactly one successor. If one or more states have multiple successors, the Kripke structure is nondeterministic
. The Kripke structure also has a designated initial state
, which represents a state in which the network can start. The Kripke structure is completely defined by the network and an initial state.
Every possible assignment of values to nodes is a state in the Kripke structure. To define the successors of a state
, we first define the next value
, for a node
(intuitively the next value is a value that the node will have when next updated, if nothing else changes).
depends on how the weighted sum of inputs to a node compares with thresholds for the node.
Then, the next value can be defined for each node, given a state
Once the next value of each node is defined, the set of successor states depends on what update rule
is used. The synchronous update rule
that was used in much past work defines a single successor of each state
in which each node is given its next value. Intuitively, every node is updated as soon as it can be, and all such nodes are updated simultaneously. Using the synchronous update rule results in a deterministic Kripke structure.
The asynchronous update rule
specifies that each successor state to
has at most one node updated to its next value (it is always possible that no nodes are updated, in other words,
is always a successor of itself). Intuitively, a particular node is chosen arbitrarily for updating. This represents a model with no timing constraints. When , node
is said to be enabled
. Using the asynchronous update rule, any node that is enabled may change after an arbitrary delay (but only one such node may change at a time). Any state that has at least one enabled node has multiple successor states, so the Kripke structure is nondeterministic.
Network behavior (under the synchronous and asynchronous update rules) was analyzed using a symbolic model checking tool, NuSMV, to test the robustness of the cell cycle model 
. NuSMV explores the paths of states starting from the initial state to check a specific property of interest.
The theory and algorithms in NuSMV are the results of several decades of research published in many books and papers, so we cannot explain them in depth. In brief, NuSMV is able to check dynamic properties of finite-state systems for infinitely many possible variations in inputs or internal non-deterministic choices by exhaustively searching the finite states of the system for individual states or loops that violate the property. NuSMV has several alternative implementations for searching the state of states. We used the implementation based on Boolean decision diagrams (BDDs), a data structure that can be used to explore large state sets relatively quickly (however, the models of the cell cycle only have a few thousand states, so any reasonable implementation of model checking should work well on them).
NuSMV has an input language, similar to a programming language, for describing the system to be checked. Descriptions in the language consist of a set of state variables ranging over discrete sets of values, along with rules that update those variables based on the previous state. These rules can be non-deterministic, meaning that state variables can be updated to several alternative values, in which case NuSMV will check the property for all of those possibilities. The NuSMV input language is naturally synchronous: time is divided into steps, and all variables are updated on each step. However, asynchronous updating can be encoded in NuSMV by exploiting non-determinism. Each reaction in SMV was coded as a separate rule updating its reactants and products. To implement the asynchronous update rule, an additional control variable was added to the rule, along with logic that only allows the rule to update if the control variable is set to a particular value that triggers that rule. At each time step, a value is non-deterministically chosen for the control variable, so at most one rule can fire at a time. To implement the synchronous update rule, the control variables are omitted from the rules so that all of them update simultaneously.
The property is written in NuSMV's logical specification language, CTL. It requires that the cell inevitably reach G1 for all of the sequences of states that occur with the chosen update rule. This property is violated if the cell cycle halts in some other state or continues without reaching G1. For the budding yeast models, G1 is considered to be the state where Sic1 and Cdh1 are 1 and all other variables are 0, and the initial state is the same except Cln3 is also 1. For fission yeast, G1 is taken to be the state where Wee1, Ste9 and Rum1 are 1 and all other variables are 0, and the initial state is the same except SK is also 1. We have also checked the more stringent (and complex) properties that the cell progresses through the correct sequence of stages as it progresses to G1. The models are not detailed enough to specify many intermediate states, but, in budding yeast, Clb5 is associated with DNA replication and Clb2 is associated with mitosis. In the final budding yeast model, as expected, a property requiring that the Clb5 go to 1 before Clb2 goes to 1, before finally returning to G1, holds for all possibly reaction delays. The final fission yeast model is even smaller than the budding yeast model, but we can check that Cdc2, the main driver protein causes both replication and mitosis, reaches its highest level.
To test whether there is selection pressure on the cells to be speed-independent, the speed-independent models for both budding yeast and fission yeast were mutated in silico
. The mutations were chosen by first choosing, with probability
, whether to add an input, delete an input, or re-weight an input. If the decision was to add an input, nodes
were chosen with equal probability and node
was added as an input to
with a non-zero weight chosen with equal probability from
. If the decision was to delete in input, a pair of nodes
were chosen with equal probability, where
was an input to
was deleted from the set of inputs of
. If re-weighting was chosen, an input was selected at random and the weight was changed with equal probability from
, excluding the current input weight.
Mutations were performed in a series of steps. At each step, mutants were checked with NuSMV, using the CTL properties above, but with a synchronous update rule. Mutants that failed this test were considered “non-viable” and discarded. The viable mutants were further checked using NuSMV and the asynchronous update rule to discover the proportion that were speed-independent. 500 viable mutants were generated at each mutation step, from 1 to 6 steps.