Parameter Synthesis by Model Checking in Formal Biochemical Space

ŠAFRÁNEK, David. Parameter Synthesis by Model Checking in Formal Biochemical Space. In IST Austria Henzinger Group Seminar. 2015.

Basic information

Original name

Parameter Synthesis by Model Checking in Formal Biochemical Space

Authors

ŠAFRÁNEK, David (203 Czech Republic, guarantor, belonging to the institution)

Edition

IST Austria Henzinger Group Seminar, 2015

---

Other information

Language

English

Type of outcome

Requested lectures

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

RIV identification code

RIV/00216224:14330/15:00084271

Organization unit

Faculty of Informatics

Keywords in English

model checking; parameter synthesis

Tags

International impact

---

Abstract

In the original language

Many quantitative dynamical models in computational systems biology are represented in the form of ordinary differential equations. Most of them are based on known first principles and are highly parametrized. Suitable wet-lab measurements and existing hypotheses about the modelled phenomena can be represented in a temporal logic and considered as constraints for the admissible parameters. Model checking and monitoring techniques known from formal verification can be used to synthesise model parameters that guarantee a given set of temporal properties. In this talk we present the scalable coloured model checking approach for parameter synthesis from LTL and CTL specifications. The method will be presented in the context of formal biochemical space that attempts to avoid the gap between formal methods and biology. On the practical side, application of the method to several biological problems will be given.