BioDiVinE

Category Cross-Omics>Pathway Analysis/Gene Regulatory Networks/Tools and Cross-Omics>Agent-Based Modeling/Simulation/Tools

Abstract BioDiVinE is a tool for exploring ‘discrete models’ of biological systems, predicting outcomes of experiments, and verifying specific properties of the model, based on techniques for ‘scalable qualitative simulation’ and analysis of integrated ‘regulatory network’ dynamics.

BioDiVinE is an ‘evolutionary branch’ of the DiVinE tool (see below...) accompanied by the GeNeSim GUI (see below...) for model management.

The contribution of BioDiVinE is three-fold. First, the tool provides a parallel on-the-fly ‘state space’ generator for the rectangular abstraction (RATS).

Second, the ‘state space’ generation algorithm employs several heuristics for reducing the extent of approximation by guiding the ‘state generator’ to avoid spurious simulations.

Finally, the embedded enumerative on-the-fly LTL ‘model checker’ allows direct application of efficient ‘parallel model checking’ algorithms to the analysis of ‘biological models’.

The manufacturer's experiments have shown that Ordinary Differential Equation (ODE) models involving up-to 20 variables resulting in reachable state spaces having around ‘10 to the 7th power’ states can be sufficiently analyzed (with responses in the order of tens of seconds), on a common cluster.

BioDiVinE also provides a graphical module that allows two-dimensional visualization of reachable state spaces.

BioDiVinE Toolset Description --

BioDiVinE employs aggregate power of network-interconnected workstations (nodes) to analyze large-scale ‘state transition systems’ whose exploration is beyond the capabilities of ‘sequential tools’.

System properties can be specified either directly in Linear Temporal Logic (LTL) or alternatively as processes describing ‘undesired behavior’ of systems under consideration (‘negative claim automata’).

From an algorithmic point of view, the tool implements a variety of novel ‘parallel algorithms’ for cycle detection (LTL model checking). By these algorithms, the entire state space is uniformly split into partitions and every partition is distributed to a particular ‘computing node’.

Each node is responsible for generating the respective state-space partition on-the-fly while storing visited states in local memory. The state space generator constructs the ‘rectangular abstraction’ transition system for a given ‘Multi-affine’ system.

The Library-level components are responsible for constructing, managing and distributing the state space. They form the core of the tool.

The tool provides two graphical user interface components SpecAff - allowing editing of ‘biological models’ in terms of ‘chemical reactions’, and SimAff - allowing visualization of the simulation results.

DiVinE tool --

DiVinE (Distributed Verification Environment) is an open source and extensible system for platform-dependent formal verification of computer systems.

DiVinE is in fact a ‘set of tools’ each of them tailored to a particular platform, like distributed-memory (DiVinE Cluster), shared-memory (DiVinE Multi-Core), external hard disks (DiVinE I-O), etc.

DiVinE in its current development phase offers mainly tools for platform-depended ‘model checking’ of finite state systems against specifications formulated in linear temporal logic (LTL).

Special DiVinE ‘branches’ focus on model-checking of probabilistic systems (Markov decision processes) - ProbDiVinE and on the analysis of complex ‘biological systems’ via BioDiVinE.

LTL model checking algorithms in DiVinE follow the ‘automata-based approach’. Algorithms find the accepting cycles in the product of the system model and a Buchi automaton for the negation of the formula.

In most sequential LTL model checkers Nested Depth-First Search and Tarjan's decomposition of strongly connected components are used for accepting cycle d etection. Unfortunately, both algorithms strongly rely on ‘depth-first search post-order’ for which the computation is known to be inherently sequential.

Therefore, these algorithms are unsuitable to be used in a ‘parallel setting’. DiVinE therefore implements ‘New algorithms’ for the parallel accepting cycle detection problem.

GeNeSim GUI --

GeNeSim is a web-based Graphical User Interface (GUI) for managing models of ‘biological interaction networks’ of two (2) types:

1) ‘Qualitative models’ defined by Piece-wise Linear Differential Equations (PLDEs).

2) ‘Quantitative models’ defined by Multi-affine Ordinary Differential Equations (MODEs).

Qualitative models -

The first type of models is directly inspired by the approach of Hidde de Jong and is compatible with the implementation of his software Genetic Network Analyzer (GNA) - (see G6G Abstract Number 20152R) up to version 6.0.

Models of this type can be created, edited and imported from GNA 5.5 and GNA 6.0 and exported to GNA 5.5, GNA 6.0, XML (old format used by DiVinE) and Systems Biology Markup Language (SBML) (subset used by GNA).

Note: See the tutorial on the creation and editing of ‘Qualitative models’ under GeNeSim, located on the BioDiVinE Wiki web-site.

Quantitative models -

The second type of models is a special case of a formalism widely used for modeling ‘biological systems’ - ODEs - restricted by allowing only ‘multi-affine equations’. These models are typically the result of systems having only ‘mass action kinetics’.

For analyzing these models, methods of discretization by hyper-rectangles have been developed by C. Belta and L.C.G.J.M. Habets and further adapted by Prof J. van Schuppen. To be able to analyze these models, additional information about concentration thresholds and initial conditions must be specified.

Models of this type can be created, edited and imported from SBML and exported to SBML and *.BIO (internal format used by the BioDiVinE tool).

Note: See the tutorial on the creation and editing of ‘Quantitative models’ under GeNeSim, located on the BioDiVinE Wiki web-site.

System Requirements

Contact manufacturer.

Manufacturer

Manufacturer Web Site BioDiVinE

Price Contact manufacturer.

G6G Abstract Number 20581

G6G Manufacturer Number 104184