Home

This is introduction to BioDiVinE 2.0. The tool that combines model checking tool BioDiVinE 1.0 with parameters estimator alias PEPMC. Both extended by new input model and in respect to it by new abstraction method that trasforms non-linear functions like Hill functions into piece-wise multi-affine functions which tools can work with.

Model checking

Model checking is an automatic technique for verifying finite state system. Finite state system means biological model that is transformed into mathematical formalism and by verifying it is meant testing satisfiability of some specification or property in form of temporal logic formula. For example in model describing two genes which products regulate each other's gene we can ask if concentration of products of these genes will exceed specified bound or if one of them will be silenced while other one wont. Here it's very important to mention that for succesful modeling of the system and correct specification of property it is needed some measurment system. In case of biological or biochemical models it is proposed using of concentration level or just some amounts of special interest called thresholds. In respect ot these thresholds it is necessary to specify also initial thresholds or conditions which indicate starting amounts of molecules. For details of writing into input file see this section.

Very important for model checking is property format. We use LTL formulas which mean Linear Temporal Logic. For more details about LTL see this link. And for more details about our format of formulas see this section.

Demonstration of model checking is in this section.

Parameter estimation

...

Acknowledgement

BioDiVinE 2.0 is developed as a part of research at Systems Biology Laboratory at Faculty of Informatics of Masaryk University.

Throughout year 2014, the development was supported by Program for Support of Student Seseach and Development Projects (in Czech) also at Faculty of Informatics.