Zadání projektů k PA054 (jaro 2014)

Projekt sestává ze tří nezávislých bloků, pro každý blok jsou volitelné varianty (mohou být libovolně promíchány až na níže specifikovaná omezení). Úspěšné řešení projektu bude sestávat z vypracování všech tří bloků (každý dle výběru). Výstupem bude report (cca 3-4 strany A4).

I - Blok modelu (10 bodů)

Výstupem bude stručný popis vybraného modelu (nejvýše 1 strana reportu).

Varianta A

Seznamte se s modelem signální dráhy ovlivňující růstový faktor (MAPK/ERK). Dráha byla probírána jako průběžný příklad na přednáškách. Vyjděte ze spojitého modelu Kholodenko 2000, který zohledňuje zpětnou vazbu způsobující oscilaci. Spojitý model je dostupný v SBML verzi na Biomodels.org.

Varianta B

Seznamte se s modelem přístupu dusíku skrz membránu E. Coli. Model je stručně popsán v tomto článku (str. 10). Model je začleněn do širšího modelu asimilace amoniaku E. Coli odkazovaného z článku (Ma, Boogerd, Goryanin: Modelling nitrogen assimilation of Escherichia coli at low ammonium concentration; publikace dostupná z domény FI).

II - Blok specifikace modelu (20 bodů)

Výstupem bude specifikace modelu ve vybraném formalismu (viz varianty níže) zapsána a dokumentována v reportu. Volba jedné z variant determinuje volbu varianty v bloku III.

Varianta A - přístup Petriho sítí

Specifikujte model prostřednictvím Petriho sítě. Zapište model v nástroji Snoopy (vytvořte spojitou i kvalitativní variantu). Hint: Model MAPK/ERK vyžaduje zachycení zpětné vazby (regulačního vztahu). To lze vyjádřit reversibilní komplexační reakcí Ras/MKKK + MAPK-PP <-> Ras/MKKK-(MAPK-PP).

Varianta B - přístup proces algeber

Specifikujte model prostřednictvím algebry BioPEPA (lze využít BioPEPA Workbench). Pro MAPK/ERK model lze uplatnit hint varianty A.

III. Blok analýzy (30 bodů)

Výstupem bude popis výsledků provedených analýz v reportu.

Varianta A - statická a kvalitativní analýza, předpokládá volbu II.A

Najděte všechny netriviální P-invarianty a T-invarianty a zkuste interpretovat jejich význam.
Zkonstruujte iniciální označkování.
Najděte vstup/výstupní T-invariant a zjistěte jeho realizovatelnost v iniciálním označkování.
Zformulujte v temporální logice vlastnost specifikující fakt, že běh realizující vstup/výstupní T-invariant je z iniciálního markingu jediné možné vstup/výstupní chování sítě. Pomocí model checkingu potvrďte/vyvraťte platnost vlastnosti.

Varianta B - kvantitativní analýza, předpokládá volbu II.B

Převeďte model do nástroje PRISM. Formulujte dle vlastního zvážení dvě různé tranzientní vlastnosti dynamiky zvoleného modelu. Použijte logiku CSL. Tyto dvě vlastnosti analyzujte prostřednictvím nástroje PRISM - pravděpodobnostní model checking (např. odhadněte pravděpodobnost s jakou vlastnost platí z daných iniciálních podmínek). Iniciální podmínky volte dle článku prezentujícího zvolený model.