Infobiotics Workbench (IBW)

Category Cross-Omics>Agent-Based Modeling/Simulation/Tools

Abstract The Infobiotics Workbench (IBW) is an integrated software suite for model design, simulation, and analysis.

IBW provides a user-friendly front-end allowing the modeler to design in- silico experiments, analyze and visualize results using its four (4) components:

1) A modeling language based on P systems which allows modular and parsimonious multi-cellular model development including geometric information.

2) A multi-compartmental stochastic simulator (mcss) based on Gillespie’ s Stochastic Simulation Algorithm for multi-cellular systems.

3) ‘Formal model analysis’ using the stochastic model checkers PRISM (see below...) and MC2 (see below...) for the study of temporal and spatial model properties.

4) Structural and parameter model optimization using evolutionary algorithms to automatically generate models whose dynamics match specified targets.

Note: Infobiotics is a computational framework implementing a synergy between executable biology, multi-compartmental stochastic simulations, formal model analysis and structural/parameter model optimization for computational systems and synthetic biology.

1) Model Specification and Building --

The specification and building of multi-cellular system models in Infobiotics is modular allowing parsimonious and incremental design.

The Infobiotics modeling language provides a multi-compartmental, stochastic and rule-based specification framework.

A model of a multi-cellular system in Infobiotics is developed as a Lattice Population P-system (LPP-system) which consists of the specification of three (3) main components that can be defined in a modular manner:

2) Multi-compartmental Stochastic Simulations --

The multi-compartmental stochastic simulator (mcss) is an application for simulating multi-compartment stochastic ‘P system models’. mcss takes a model specified in Systems Biology Markup Language (SBML) and simulates it using the multi-compartment Gillespie algorithm.

A large number of spatially-distributed compartments containing many chemical species, reactions and transportation channels can be simulated.

Templates can be specified which define a set of reactions which can be reproduced in many compartments.

mcss is being used to develop Systems/Synthetic Biology computational models of plant systems and bacterial colonies.

mcss Model specification -

CellDesigner (see G6G Abstract Number 20159) can used to graphically design a model, which can then be exported as an SBML Level 2 model.

3) Model Formal Analysis using Model Checking --

pmodelchecker is an application that facilitates the use of formal model analysis using Model Checking of spatio-temporal properties of P system models developed within the Infobiotics workbench.

pmodelchecker receives as input a model developed as specified (see Model Specification and Building above ...) and a list of temporal logic formulas formalizing some spatio-temporal properties to be checked against the dynamics of the model.

pmodelchecker uses two (2) different stochastic model checkers, PRISM and MC2.

When using PRISM it generates a model in the reactive modules language needed in PRISM in order to check the input logic formulas.

When using MC2 it generates the needed simulation samples by running mcss, the multi-compartmental simulator (see Multi-compartmental Stochastic Simulations above...).

4) Structure and Parameter Optimization with poptimizer --

poptimizer is an application for optimizing the structure and parameters of ‘stochastic P system models’ using evolutionary algorithms.

poptimizer takes a library of modules that represent basic biological processes of interest and combines them in many different ways to discover a possible assembly that mimics the behavior of the target data.

During the search process, each model is evaluated by simulating its behavior with mcss.

poptimizer and mcss (as stated above…) are being used to develop Systems and Synthetic Biology computational models of bacterial colonies and plant systems.

poptimizer Models --

The models built by poptimizer have a flexible structure and parameters. A particular model is composed by a set of elementary modules (previously specified in a library) that act as the building blocks.

The user can define their own module library based on specific knowledge or simply on elementary biological motifs described in the Systems Biology literature.

While certain modules can have fixed rules and kinetic constants (fixed module library), others can be instantiated with different objects (proteins, genes, etc.) and parameter values (non-fixed library).

Many kinetic constants referring to well-known reactions can be taken from the literature and introduced in the library, where others need to be evolved by the parameter optimization methods available in poptimizer.

poptimizer Model Structure Optimization --

The optimization of the model structure is concerned with the choice of which modules should compose the model. The number of modules and their corresponding instantiation (according to a choice of different objects) is also explored to minimize the error between the output data generated by the model and the target data.

A genetic algorithm (GA) that selects, recombines, and mutates different sets of modules is used to optimize the model structure.

poptimizer Model Parameters Optimization --

The optimization of the model parameters is concerned with learning the appropriate kinetic constants corresponding to each one of the rules specified in the modules. When the kinetic constants are Not known from literature, the module library specifies the parameter ranges (and a choice of linear/logarithmic scale) for each kinetic constant.

The parameter optimization methods currently available include genetic algorithms (GA), differential evolution (DE), opposition differential evolution (ODE), and the covariance matrix adaptation evolution strategy (CMA-ES).


PRISM is a probabilistic model checker, a tool for formal modeling and analysis of systems which exhibit random or probabilistic behavior.

It supports three (3) types of probabilistic models: discrete-time Markov chains (DTMCs), continuous-time Markov chains (CTMCs) and Markov decision processes (MDPs), plus extensions of these models with costs and rewards.

PRISM has been used to analyze systems from a wide range of application domains, including communication and multimedia protocols, randomized distributed algorithms, security protocols, biological systems and many others.

MC2 --

MC2 (PLTLc) is a Monte Carlo Model Checker for properties written in Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc). The model checker takes as input a set of traces in the form of a simulation output file.

It also takes as input a query file containing a list of PLTLc properties, and returns for each property the probability that the set of traces satisfies the property.

MC2 (PLTLc) can also calculate the probabilistic domains of free variables within a property; thus it is easy to calculate the distribution of features, such as times at which peaks occur.

MC2 (PLTLc) can operate with stochastic/deterministic simulation output, deterministic parameter scan output or even wet-lab data.

System Requirements

Contact manufacturer.


Manufacturer Web Site Infobiotics Workbench (IBW)

Price Contact manufacturer.

G6G Abstract Number 20592

G6G Manufacturer Number 104195