Parameter Synthesis by Model Checking in Formal Biochemical Space

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F15%3A00084271" target="_blank" >RIV/00216224:14330/15:00084271 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Parameter Synthesis by Model Checking in Formal Biochemical Space

Popis výsledku v původním jazyce

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 parametersthat 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 thatattempts to avoid the gap between formal methods and biology. On the practical side, application of the method to several biological problems will be given.

Název v anglickém jazyce

Parameter Synthesis by Model Checking in Formal Biochemical Space

Popis výsledku anglicky

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 parametersthat 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 thatattempts to avoid the gap between formal methods and biology. On the practical side, application of the method to several biological problems will be given.

Druh

O - Ostatní výsledky

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů