Bakalářská práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

Škálovatelná syntéza parametrů pro hypotézy formulované v logice CTL

Scalable Parameter Synthesis from CTL Hypotheses

Samuel Pastva, učo 410286
Anotace

Hlavným cieľom tejto práce je navrhnúť a implementovať paralelný algoritmus pre výpočet problému syntézy parametrov pre biochemické systémy a CTL hypotézy operujúci v distribuovanej pamäti. Výsledný algoritmus je založený na farebnom CTL overovaní modelov. Aplikovateľnosť a škálovateľnosť algoritmu sú demonštrované na biochemických modeloch založených na obyčajných diferenciálnych rovniciach. Taktiež diskutujeme možné heuristiky na delenie stavového priestoru týchto modelov.

Abstract

The main goal of this thesis is to design and implement a parallel and distributed memory algorithm for computing the parameter synthesis problem for biochemical systems and CTL hypotheses. The resulting algorithm is based on coloured CTL model checking. The applicability and scalability of the algorithm is successfully demonstrated on biochemical models based on ordinary differential equations. We also discuss possible heuristics for state space partitioning of these models.

Klíčová slova
Coloured Model Checking CTL Distributed Memory Parameter Synthesis Problem Systems Biology ODE Model Thomas Network Farebné Overovanie Modelov Distribuovaná Pamäť Problém Syntézy Parametrov Systémová Biológia
Zadání práce
Úkolem je navrhnout a implementovat distribuovaný algoritmus pro syntézu parametrů modelů biochemických systémů, který vychází z distribuovaného algoritmu pro ověřování modelu pro logiku CTL [Brim et al.]. Algoritmus by měl sledovat analogický přístup, který byl použit pro syntézu parametrů z hypotéz formulovaných v temporální logice LTL, tzv. barevný model-checking [Barnat et al.]. Funkčnost výsledného programu se pokusit ověřit na vhodné případové studii biochemického systému.
Administrativní informace
Práce zkontrolována:
19. 5. 2015 07:25, prof. RNDr. Luboš Brim, CSc.
Plný text práce
592 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
17. 6. 2015
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Luboš Brim, CSc.
KTP FI MU

Oponent

doc. RNDr. David Šafránek, Ph.D., učo 3159
KSUZD FI MU

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
  • BRIM, Luboš; Jitka ŽIDKOVÁ a Karen YORAV. Assumption-based distribution of CTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2005, roč. 7, č. 1, s. 61-73, 14 s. ISSN 1433-2779.
  • 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. ISSN 1545-5963. Dostupné z: https://doi.org/10.1109/TCBB.2011.110.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.