Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu PA 054: Formální modely v systémové biologii David Šafránek 26.2.2010 Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu Obsah Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu Informace o předmětu Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu ZÁKLADNÍ POJMY A PRINCIPY POJEM IN SILICO MODELU Obsah Informace o předmětu Úvod ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Náplň předmětu • in silico model jako formální systém • metody abstrakce používané pro vytvoření modelu • aplikace formálních metod: • přístupy ke specifikaci modelu • přístupy k analýze modelu • analytické metody • algoritmické metody • seznámení s nástroji • stránky předmětu: http: //www. f i. muni. cz/^xsaf ranl/PA054/ Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Osnova Základní pojmy a principy Virtuální laboratoř aneb in silico model jako formální systém Struktura modelu - biologické sítě Sémantika modelu - modely dynamiky Petriho sítě, Boolovské sítě, rule-based formalismy, ... Model checking a validace modelu Spojité deterministické modely, jejich diskretizace a analýza Stochastické modely a jejich analýza Modely s neurčitostí Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu Požadavky na ukončení • zkouška ústní • Bc zk, Mgr k: celkový přehled • Mgr zk: konkrétní téma + vědecký článek/kapitola knihy Úvod Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu ZÁKLADNÍ POJMY A PRINCIPY POJEM IN SILICO MODELU Obsah Úvod Cü SB: Pochopit a předvídat chováni živého organismu Organismus = komplexní systém Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Cü SB: Pochopit a předvídat chováni živého organismu Organismus = komplexní systém _ Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Podcíí SB: Pochopit a předvídat chováni živé buňky Živá buňka = komplexní systém genotyp —-T ■^ metabolismus, proteosynteza = emergentnívlastnosti Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Hudba života I - Genome CD Music of Life by Denis Noble X Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Hudba života I - Genome CD Music of Life by Denis Noble Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Hudba života I - Genome CD Music of Life by Denis Noble gene ^tf^F okoli \^ COde J y^ pratředi }\%\ zivy \^ dynamicky ^ system \^ Úvod Hudba života II - Komplexní systém • komplexní dynamický jev v čase a prostoru • např. kvadrofonní zvukový záznam z deštného pralesa... • zvuky se vzájemně ovlivňují...emergují v komplexní souzvuky... • pohled 1 (lékař): jak odstranit nezdravé disharmonie? • pohled 2 (biotechnolog): jak upřednostnit určité souzvuky před jinými? • předpovídat a pochopit emergentní vlastnosti • identifikovat a pochopit jednotlivé interakce • identifikovat a pochopit vzájemnou součinnost interakcí Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Živý vs. formální systém živy (biologicky) system paralelismus nedeterminismus komunikace hierarchie Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Živý vs. formální systém Informace o předmětu Základni pojmy a principy Pojem in silico modelu Abstrakce - formální model > živy dynamicky system g -► formálni model in vitro/in vivo S©M Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Úplatném formálního modelu rekonstrukce sítí databáze biol. znalostí + literatura J<ÍgcP biologická sít hypotézy specifikace modelu SBML, diferenciální rovnice, boolovská sít, Petriho sít, ... validace modelu genové reportéry, DNA microarray, hmotnostní spektrometrie, ... objevené vlastnosti ■<--------------------------------------- dotazy na model analýza modelu statická analýza, numerická simulace, analytické metody, model checking verifikace hypotéz, detekce vlastností vyvození nových hypotéz Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Úplatném formálního modelu rekonstrukce sítí databáze biol. znalosti + literatura validace modelu genové reportéry, DNA microarray, hmotnostní spektrometrie, ... specifikace modelu SBML, diferenciální rovnice, boolovská sít, Petriho sít, ... analýza modelu statická analýza, numerická simulace, analytické metody, model checking verifikace hypotéz, detekce vlastnosti vyvozeni nových hypotéz .Q Úvod Co poskytují formální metody? • tzv. "model-based" přístup k systémovému inženýrství • specifikace • jednoznačný popis modelu a jeho vlastností • konečný popis nekonečných objektů • kompaktní popis rozsáhlých objektů • modulární/hierarchická struktura • analýza • formální sémantika • porovnávání modelů a jeho částí (equivalence checking) • verifikace modelu vzhledem ke specifikovaným vlastnostem (model checking) • detekce vlastností modelu • estimace a syntéza parametrů Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Tradiční uplatnění formálních metod System Engineering (HW/SW) system verifikace konstrukce požadovane vlastnosti specifikace. specifikované vlastnosti Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Uplatnění formálních metod v systémové biologii System Re-engineering (pochopení biologických systémů) system C validace predikce emergentni vlastnosti Cxjkonstrukcj^ ) 4 ^identifikace]^ model analyzované vlastnosti Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Uplatnění formálních metod v systémové biologii - vize Living Systems Engineering (syntetická biologie) system verifikace konstrukce požadovane vlastnosti specifikace. specifikované vlastnosti Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Tradiční matematické metody vs. formální metody matematické metody (1 stoichiometricka analýza diferenciální (spojité) modely numerické simulace analytické metody formálni metody Jl rule-based specifikace diskrétni modely diskrétni simulace model checking equivalence checking Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Tradiční matematické metody vs. formální metody matematické metody (1 formálni metody Jl rule-based specifikace stoichiometricka analýza <; diferenciální (spojité) modely numerické simulace diskrétni modely diskrétni simulace É model checking analytické metody equivalence checking Fisher J. and Henzinger T.A., Dichotomies between computational and mathematical models (Correspondence), in Nature Biotechnology , vol. 26, no. 7, pp. 737-8;738-9, 2008 Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Přehled formálních modelů používaných v SB ^A. casove a hybridní automaty rule-based Markovovy procesové kalkulv procesy kalkuly \% Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Přehled formálních metod používaných v SB \ enumerativni cľiskretni model checking symbolicky simulace model checking formálni metody real-time model checking ra,d,podb„oM„ístatisticky Monte-Carlo model checking „„,,., '„„ slmulace / \ Úvod Příklady aplikací formálních metod v SB Diskrétní modely (tzv. "executable" (spustitelné) modely) • simulace diferenciace buněk v hádátku obecném (Caenorhabditis elegans) • využití StateCharts (rozšířené (hierarchické) automaty) Fisher J., Piterman N., Hubbard J., Stern M., and Harel D. Computational insights into C. elegans vulval development. PNAS 102(6):1951-1956, 2005. • využití Life Sequence Charts (scénáře událostí v čase) Kam N., Kugler H., Marelly R., Appleby L., Fisher J., A. Pnueli, D. Harel, M.J. Stern, and E.J.A. Hubbard, A scenario-based approach to modeling development: A prototype model of C. elegans vulval fate specification , in Developmental Biology, Elsevier, August 2008 • aplikace model checkingu Fisher J., Piterman N., Hajnal A., and Henzinger, T.A. Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development. PLoS Computational Biology. 3(5):e92, 2007. • využití Petriho sítí N. Bonzanni, E. Krepska, K.A. Feenstra, W. Fokkink, T. Kielmann, H. Bal, and J. Heringa, Executing multicellular differentiation: Quantitative predictive modelling of C.elegans vulval development, 25(16):2049-56, Bioinformatics Aug 2009. Úvod Příklady aplikací formálních metod v SB Procesové kalkuly • modelovania simulace signální dráhy RTK-MAPK A. Regev, W. Silverman, E. Shapiro, "Representation and simulation of biochemical processes using the pi-calculus process algebra." Pacific Symposium on Biocomputing. Pacific Symposium on Biocomputing (2001), pp. 459-470. • analýza hypotalamických drah pro regulaci váhy člověka Aviv Regev, Ekaterina M. Panina, William Silverman, Luca Cardelli, Ehud Shapiro. "BioAmbients: An Abstraction for Biological Compartments". Theoretical Computer Science, Special Issue on Computational Methods in Systems Biology. Volume 325, Issue 1, 28 September 2004, Pages 141-167. Elsevier. • modelování a simulace efektu štepení ribozomální RNA při transkripci (kvasinka) Federica Ciocchetta, Jane Hillston, Martin Kos and David Tollervey. Modelling Co-Transcriptional Cleavage in the Synthesis of Yeast Pre-rRNA, in Theoretical Computer Science 2008 • modelování ERK signální dráhy (BioPEPA) Muffy Calder, Stephen Gilmore, and Jane Hillston. Modelling the influence of RKIP on the ERK signalling pathway using the stochastic process algebra PEPA. In Transactions on Computational Systems Biology VII. number 4230 in LNCS. Snrimrer. 1-23 2006. Úvod Příklady aplikací formálních metod v SB Diskrétní abstrakce spojitých modelů a jejich model checking simulace genetické regulace ovlivňující sporulaci v Bacillus subtilis H. de Jong, J. Geiselmann, G. Batt, C. Hernandez and M. Page (2004) Qualitative simulation of the initiation of sporulation in Bacillus subtilis Bulletin of Mathematical Biology, 66(2):261-300 • využití model checkingu v syntetické biologii G. Batt, C. Belta and R. Weiss (2008) Temporal logic analysis of gene networks under parameter uncertainty IEEE Transactions on Circuits and Systems and IEEE Transactions on Automatic Control, Joint Special Issue on Systems Biology, pp 215-229 • využití model checkingu při analýze transportu dusíku do buňky E. coli J. Barnat, L. Brim, I. Cerna, S. Drazan, J. Fabrikova, J. Lanik, D. Šafránek, and H. Ma. BioDiVinE: A Framework for Parallel Analysis of Biological Model. In Proceedings of 2nd International Workshop on Computational Models for Cell Processes (COMPMOD 2009), pp. 31-45, EPTCS 6, 2009. Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu Obsah Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Centrální dogma .i jr*^A Transcription i^W-i v DNA *^ ħP|r " Biological Function Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Genotyp —> Fenotyp Hierarchie interakcí SITE INTERAKCI Informace o předmětu Úvod Základní pojmy a principy Pojem in silico modelu Základní molekuly organizmu • DNA • kyselina deoxyribonukleová • složena ze dvou řetězců nukleotidů {A, G, C, 7"} • primární struktura — sekvence nukleotidů • sekundární struktura — šroubovice (double helix) • stabilní molekula • obsahuje genetický kód (genom) • RNA • kyselina ribonukleová • zpravidla jeden řetězec nukleotidů {A, G, C, U} • nestabilní molekula • přenáší genetickou informaci • několik typů — mRNA (informační), tRNA (transferová), rRNA Informace o předmětu ZÁKLADNÍ POJMY A PRINCIPY Pojem in silico modelu Základní molekuly organizmu Cylotiíi* | c | í i - | a ■a u I i O ■a o u u % o u OU3■ A3 + A4 + A5 (r2) A4 + A5 ->■ 342 fc>; a3 -+ • substráty — {^1,^2, ^3, ^4,45} • reakční komplexy — {A1} 3A2, A3,2Ai + A2, A3 + A4 + A5,A4 + A5} Pojem in silico modelu Shrnuti • biologický systém definován interakcemi mezi jeho komponentami • interakce jsou určeny základními zákony chemie ale i evolučním vývojem • syntaxí modelu organismu je sít reakcí mezi komponentami (komplexy substrátů) • sémantikou modelu organismu rozumíme jeho dynamiku (vývoj substrátů v čase) Pojem in silico modelu Literatura Ul Kita no, H. Looking beyond the details: a rise in system-oriented approaches in genetics and molecular biology. Curr Genet., 2002. 13 Palsson, B. Systems Biology: Properties of Reconstructed Networks. Cambridge University Press, 2006. 3 Alon, U. An Introduction to Systems Biology: Design Principles of Biological Circuits. Chapman & Hall, 2006. 2 Bower, J.M. & Bolouri, H. Computational Modeling of Genetic and Biochemical Networks. Bradford Book, 2001. 3 Noble, D. The Music of Life: Biology Beyond the Genome Oxford University Press, 2006.