Limits...
An overview of existing modeling tools making use of model checking in the analysis of biochemical networks.

Carrillo M, Góngora PA, Rosenblueth DA - Front Plant Sci (2012)

Bottom Line: Recently, model checkers have appeared in computer tools for the analysis of biochemical (and gene regulatory) networks.Next, our overview focuses on direct applications of existing model checkers, as well as on algorithms for biochemical network analysis influenced by model checking, such as those using binary decision diagrams (BDDs) or Boolean-satisfiability solvers.We conclude with advantages and drawbacks of model checking for the analysis of biochemical networks.

View Article: PubMed Central - PubMed

Affiliation: Departamento de Ciencias de la Computación, Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México México D.F., México.

ABSTRACT
Model checking is a well-established technique for automatically verifying complex systems. Recently, model checkers have appeared in computer tools for the analysis of biochemical (and gene regulatory) networks. We survey several such tools to assess the potential of model checking in computational biology. Next, our overview focuses on direct applications of existing model checkers, as well as on algorithms for biochemical network analysis influenced by model checking, such as those using binary decision diagrams (BDDs) or Boolean-satisfiability solvers. We conclude with advantages and drawbacks of model checking for the analysis of biochemical networks.

No MeSH data available.


A state-transition graph of example in Figure 2 showing asynchrony.
© Copyright Policy - open-access
Related In: Results  -  Collection

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

Figure 3: A state-transition graph of example in Figure 2 showing asynchrony.

Mentions: A state-transition system T is now obtained as follows. T has a transition (edge) from s to (kx1 (s), … , kxn(s)) if and only if ki (s) ≠ si for at most one i. Note that a state may have more than one successor. The state-transition system for our example is exhibited in Figure 3.


An overview of existing modeling tools making use of model checking in the analysis of biochemical networks.

Carrillo M, Góngora PA, Rosenblueth DA - Front Plant Sci (2012)

A state-transition graph of example in Figure 2 showing asynchrony.
© Copyright Policy - open-access
Related In: Results  -  Collection

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

Figure 3: A state-transition graph of example in Figure 2 showing asynchrony.
Mentions: A state-transition system T is now obtained as follows. T has a transition (edge) from s to (kx1 (s), … , kxn(s)) if and only if ki (s) ≠ si for at most one i. Note that a state may have more than one successor. The state-transition system for our example is exhibited in Figure 3.

Bottom Line: Recently, model checkers have appeared in computer tools for the analysis of biochemical (and gene regulatory) networks.Next, our overview focuses on direct applications of existing model checkers, as well as on algorithms for biochemical network analysis influenced by model checking, such as those using binary decision diagrams (BDDs) or Boolean-satisfiability solvers.We conclude with advantages and drawbacks of model checking for the analysis of biochemical networks.

View Article: PubMed Central - PubMed

Affiliation: Departamento de Ciencias de la Computación, Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, Universidad Nacional Autónoma de México México D.F., México.

ABSTRACT
Model checking is a well-established technique for automatically verifying complex systems. Recently, model checkers have appeared in computer tools for the analysis of biochemical (and gene regulatory) networks. We survey several such tools to assess the potential of model checking in computational biology. Next, our overview focuses on direct applications of existing model checkers, as well as on algorithms for biochemical network analysis influenced by model checking, such as those using binary decision diagrams (BDDs) or Boolean-satisfiability solvers. We conclude with advantages and drawbacks of model checking for the analysis of biochemical networks.

No MeSH data available.