Informační systém Masarykovy univerzity 

Archiv závěrečné práce Samuel Pastva FI B-IN PDS

česky | in English

Agenda:
Změnit agendu. Adresa v ISu:

Masarykova univerzita

Fakulta informatiky

bakalářský studijní program/obor:
Informatika/Paralelní a distribuované systémy

Samuel Pastva

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

Scalable Parameter Synthesis from CTL Hypotheses

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.

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í: Ú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.

Jazyk práce: angličtina

  • Zadáno/změněno 18. 6. 2015 07:27, Eva Drštková
  • Záznam založen 8. 4. 2015 14:53, Lucie Pekárková
  • Zveřejnit od 18. 5. 2015 11:16, Alena Dvořáková
  • Práce převzata 18. 5. 2015 11:16, Alena Dvořáková

Obhajoba bakalářské práce

  • Proběhla 17. 6. 2015, práce byla úspěšně obhájena.

Vedoucí:

  • prof. RNDr. Luboš Brim, CSc., KTP FI MU, Katedra teorie programování - Fakulta informatiky

Oponent:

Plný text práce
Příloha

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. 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. doi:10.1109/TCBB.2011.110.

Citační záznam

Citace dle ISO 690: LaTeX | HTML | text | BibTeX | Wikipedie

Kontrola závěrečné práce

Práce zkontrolována: 19. 5. 2015 07:25, prof. RNDr. Luboš Brim, CSc.


Nástroje.Seřadit vzestupně.Seřadit sestupně. Spočítat nepřečtené soubory ve složkách. Spočítat velikost složek. Zobrazit mapu souborů. Napřed složky, pak soubory.Seřadit vzestupně.Seřadit sestupně. Složka či souborSeřadit vzestupně.Seřadit sestupně. Vložil/aSeřadit vzestupně.Seřadit sestupně. VloženoSeřadit vzestupně.Seřadit sestupně. Expirace: Seřadit vzestupně.Expirace: Seřadit sestupně.
Nástroje.Tato složka.  Archiv závěrečné práce Samuel Pastva FI B-IN PDS /fi_b/Pekárková, L. 8.  4. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor annotation_english.txt, 481 B, holý textAnotace anglicky annotation_english.txtPastva, S.18.  5. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor annotation.txt, 481 B, holý textAnotace česky annotation.txtPastva, S.18.  5. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor keywords.txt, 218 B, holý textKlíčová slova keywords.txtPastva, S.18.  5. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor thesis.pdf, 592 KB, PDF Soubor thesis.txt, 57,7 KB, holý textPlný text práce thesis.pdfPastva, S.18.  5. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor sam.pdf, 26,8 KB, PDF Soubor sam.txt, 2,3 KB, holý textPosudek oponenta sam.pdfŠafránek, D. 5.  6. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor r_pastva.pdf, 28,9 KB, PDF Soubor r_pastva.txt, 2 KB, holý textPosudek vedoucího r_pastva.pdfBrim, L. 2.  6. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Nástroje.Soubor Distributed-CTL-Model-Checker.zip, 2 MB, archív ZIPPříloha Distributed-CTL-Model-Checker.zipPastva, S.18.  5. 2015
Číst smí:
• kdokoliv v Internetu
Nikdo nemá právo vkládat.Nikdo nemá právo spravovat.Žádný atribut.
Prohlédnout tuto složku po přihlášení do ISu (znáte-li svoje heslo do ISu, můžete zde vidět více souborů)

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 20. 9. 2017 07:39, 38. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému