Limits...
Approximating Attractors of Boolean Networks by Iterative CTL Model Checking.

Klarner H, Siebert H - Front Bioeng Biotechnol (2015)

Bottom Line: Our main result is an alternative approach which is based on the iterative refinement of an initially poor approximation.The algorithm detects so-called autonomous sets in the interaction graph, variables that contain all their regulators, and considers their intersection and extension in order to perform model checking on the smallest possible state spaces.A benchmark, in which we apply the algorithm to 18 published Boolean networks, is given.

View Article: PubMed Central - PubMed

Affiliation: Fachbereich Mathematik und Informatik, Freie Universität Berlin , Berlin , Germany.

ABSTRACT
This paper introduces the notion of approximating asynchronous attractors of Boolean networks by minimal trap spaces. We define three criteria for determining the quality of an approximation: "faithfulness" which requires that the oscillating variables of all attractors in a trap space correspond to their dimensions, "univocality" which requires that there is a unique attractor in each trap space, and "completeness" which requires that there are no attractors outside of a given set of trap spaces. Each is a reachability property for which we give equivalent model checking queries. Whereas faithfulness and univocality can be decided by model checking the corresponding subnetworks, the naive query for completeness must be evaluated on the full state space. Our main result is an alternative approach which is based on the iterative refinement of an initially poor approximation. The algorithm detects so-called autonomous sets in the interaction graph, variables that contain all their regulators, and considers their intersection and extension in order to perform model checking on the smallest possible state spaces. A benchmark, in which we apply the algorithm to 18 published Boolean networks, is given. In each case, the minimal trap spaces are faithful, univocal, and complete, which suggests that they are in general good approximations for the asymptotics of Boolean networks.

No MeSH data available.


Related in: MedlinePlus

An illustration of the how the iterative refinement algorithm confirms that  of the MAPK network is complete. Altogether 12 restricted systems are model checked instead of the single full system. A more detailed description is given in the main text.
© Copyright Policy
Related In: Results  -  Collection

License
getmorefigures.php?uid=PMC4562258&req=5

Figure 4: An illustration of the how the iterative refinement algorithm confirms that of the MAPK network is complete. Altogether 12 restricted systems are model checked instead of the single full system. A more detailed description is given in the main text.

Mentions: Figure 4 is an illustration of the steps performed during the iterative refinement for the MAPK network. The information is represented as a decision tree. The root represents the initial and trivially complete set P : = {ε}. Boxes are split into a left side, representing the size /U/ of a minimal autonomous set (or an extension), and a right hand side that is split vertically into cells that contain the numbers /Dq/ of fixed variables for each minimal trap space q of (U, F/U). Boxes are colored according to whether (U, F/U) is trap-space-free (white) or not in which case model checking is required to find out whether the minimal trap spaces of (U, F/U) are complete (failure criterion). Boxes with more than one minimal trap space are outlined in red to emphasize that a decision process between competing trap spaces exists. The intersection of several autonomous sets is indicated by ⊗ but occurs for this network only for the inputs. Arcs are labeled by the number of variables that are fixed during percolations, i.e., (see line 22 in Figure 3). If a restricted network is trap-space-free, the extension is indicated by a dashed arc. Along each branch of the decision tree, the number of fixed and oscillating variables must add up to 53. The bottom branch, for example, starts with four fixed variables, percolates seven more, extends an autonomous set whose restriction consists of four variables and is trap-space-free, finds a single trap space with three fixed variables and finishes as the remaining trap space is minimal (and 4 + 7 + 3 + 0 + 39 = 53).


Approximating Attractors of Boolean Networks by Iterative CTL Model Checking.

Klarner H, Siebert H - Front Bioeng Biotechnol (2015)

An illustration of the how the iterative refinement algorithm confirms that  of the MAPK network is complete. Altogether 12 restricted systems are model checked instead of the single full system. A more detailed description is given in the main text.
© Copyright Policy
Related In: Results  -  Collection

License
Show All Figures
getmorefigures.php?uid=PMC4562258&req=5

Figure 4: An illustration of the how the iterative refinement algorithm confirms that of the MAPK network is complete. Altogether 12 restricted systems are model checked instead of the single full system. A more detailed description is given in the main text.
Mentions: Figure 4 is an illustration of the steps performed during the iterative refinement for the MAPK network. The information is represented as a decision tree. The root represents the initial and trivially complete set P : = {ε}. Boxes are split into a left side, representing the size /U/ of a minimal autonomous set (or an extension), and a right hand side that is split vertically into cells that contain the numbers /Dq/ of fixed variables for each minimal trap space q of (U, F/U). Boxes are colored according to whether (U, F/U) is trap-space-free (white) or not in which case model checking is required to find out whether the minimal trap spaces of (U, F/U) are complete (failure criterion). Boxes with more than one minimal trap space are outlined in red to emphasize that a decision process between competing trap spaces exists. The intersection of several autonomous sets is indicated by ⊗ but occurs for this network only for the inputs. Arcs are labeled by the number of variables that are fixed during percolations, i.e., (see line 22 in Figure 3). If a restricted network is trap-space-free, the extension is indicated by a dashed arc. Along each branch of the decision tree, the number of fixed and oscillating variables must add up to 53. The bottom branch, for example, starts with four fixed variables, percolates seven more, extends an autonomous set whose restriction consists of four variables and is trap-space-free, finds a single trap space with three fixed variables and finishes as the remaining trap space is minimal (and 4 + 7 + 3 + 0 + 39 = 53).

Bottom Line: Our main result is an alternative approach which is based on the iterative refinement of an initially poor approximation.The algorithm detects so-called autonomous sets in the interaction graph, variables that contain all their regulators, and considers their intersection and extension in order to perform model checking on the smallest possible state spaces.A benchmark, in which we apply the algorithm to 18 published Boolean networks, is given.

View Article: PubMed Central - PubMed

Affiliation: Fachbereich Mathematik und Informatik, Freie Universität Berlin , Berlin , Germany.

ABSTRACT
This paper introduces the notion of approximating asynchronous attractors of Boolean networks by minimal trap spaces. We define three criteria for determining the quality of an approximation: "faithfulness" which requires that the oscillating variables of all attractors in a trap space correspond to their dimensions, "univocality" which requires that there is a unique attractor in each trap space, and "completeness" which requires that there are no attractors outside of a given set of trap spaces. Each is a reachability property for which we give equivalent model checking queries. Whereas faithfulness and univocality can be decided by model checking the corresponding subnetworks, the naive query for completeness must be evaluated on the full state space. Our main result is an alternative approach which is based on the iterative refinement of an initially poor approximation. The algorithm detects so-called autonomous sets in the interaction graph, variables that contain all their regulators, and considers their intersection and extension in order to perform model checking on the smallest possible state spaces. A benchmark, in which we apply the algorithm to 18 published Boolean networks, is given. In each case, the minimal trap spaces are faithful, univocal, and complete, which suggests that they are in general good approximations for the asymptotics of Boolean networks.

No MeSH data available.


Related in: MedlinePlus