Tématem práce je oblast syntézy parametrů dynamických modelů dle temporální specifikace s aplikací na modely ve výpočetní systémové biologii. V poslední době byl na FI vyvinut a implementován algoritmus tzv. barevného model checkingu, který tento problém řeší. Dosud však tato implementace nebyla doladěna do uživatelsky přívětivé podoby a nebyla řádně otestována. Cílem této práce je implementaci finalizovat, řádně otestovat na reálných modelech a kriticky vyhodnotit použitelnost této metodologie pro systémovou biologii.

V teoretické části se student seznámí s existujícími algoritmy a implementacemi pokročilé varianty abstrakce diferenciálních modelů biologických systémů kombinujících sigmoidální kinetiku a kinetiku dle zákona zachování hmoty (zejména nástroj BioDiVinE v1.5 vypracovaný v rámci studentského projektu a jeho modul PEPMC). Dále se student podrobně seznámí s biologicky motivovanými modely dle pokynů vedoucího.

V praktické části student provede následující dílčí úlohy:

• navrhne a realizuje refaktorizaci modulu PEPMC v rámci nástroje BioDiVinE v1.5 za účelem zlepšení uživatelské přívětivosti
• náležitě dokumentuje refaktorizovaný kód za účelem budoucího rozšiřování nástroje
• vytvoří sadu biologicky motivovaných modelů na různé úrovni složitosti
• rigorózně otestuje rozšíření parametrického prostředí barevného LTL model checkingu o pokročilou variantu abstrakce na sadě modelů
• kriticky vyhodnotí efektivnost a praktickou použitelnost nástroje
• rozmyslí rozšíření metody na neortogonální abstrakce parametrického prostoru

Refaktorizovaná verze nástroje bude dokumentována a publikována na githubu. Součástí textu práce bude sada jednodušších příkladů i reálných biologických modelů řádně anotovaná dle standardů systémové biologie.

Literatura:

• Radu Grosu, Grégory Batt, Flavio H. Fenton, James Glimm, Colas Le Guernic, Scott A. Smolka, Ezio Bartocci: From Cardiac Cells to Genetic Regulatory Networks. CAV 2011: 396-411
• BARNAT, Jiří, Luboš BRIM, Adam KREJČÍ, Adam STRECK, David ŠAFRÁNEK, Martin VEJNÁR a Tomáš VEJPUSTEK. On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Transactions on Computational Biology and Bioinformatics, Los Alamitos: IEEE Computer Society, 2012, roč. 9, č. 3, s. 693-705.