Formal Biochemical Space with Semantics in Kappa and BNGL David Šafránek with T. Děd, M. Troják, M. Klement, J. Salagovič, L. Brim sybila v svsiems bioloav lal systems biology laboratory Systems Biology Laboratory Masaryk University Brno SASB 2015, Saint-Malo, France 8 September 2015 Background and Motivation Comprehensive Modelling Platform (CMP) Processes Cyanobactenum in its environment Environmental processes Cellular pnooBSM* "O r -^pi-jit or, ?rd photosynthesis -o Carbon concentrating mechanism (CCM) "O respiration "O Clock "O Mr--arnli-rr ^ Transport Cellular processes Respiration Clock Respiration and Photosynthesis Annotations Models Relations Reactions Metabolism Transport ■medium Contains: \hv ako d membrane ■\ater ohctor www.e-cyanobacterium.org Safränek et al. Formal Biochemical Space Background and Motivation Biochemical Space in the context of CMP Repository of kinetic models I.. , j i |-1 Model space \-1 Species Reactions Parameters Biochemical space Entities Reactions Annotation need for easy-to-understand but yet formal description of biological processes tackle the complexity - combinatorial explosion ^» systems biology laboratory Šafránek et al. Formal Biochemical Space Annotation Standards Connection to Bioinformatics Safränek et al. Formal Biochemical Space Biochemical Space Eliminating the Gap Between Biology and Math Cellular processes formalization Models annotation biophysics employs a lot of indirect approximation in models combining rule-based approach with reaction-based approach allows compact mechanistic description mapping the models to such a description allows better and faster understanding sybilad ^» systems biology laboratory Šafránek et al. Formal Biochemical Space Abstraction from structural details Biology - graph "isomorphism" - 700 different deviations ^—^ ■ Unphosphorylated protein Serine residue phosphorylated protein ■ Threonine residue phosphorylated protein Both residues phosphorylated protein Šafránek et al. BCS abstraction - mixture —»- order not important - 84 different deviations Formal Biochemical Space 6 Biochemical Space Language Key Features • stoichiometry —y enumerated shortened forms • states —>• encoding different forms of an entity • composition • full —> complexation, coexistence in a solution • partial —>• inner structure of interest • locations —> spatial organisation • variables —>• wildcards in definitions sybilaH systems biology laboratory Šafránek et al. Formal Biochemical Space Differences from Other Formalisms BioChemical Space Language is a rule-based language which has: • no binding sites —> details of complexes formation abstracted out • abstract from bonds • annotation purpose —> specify what interacts with what without details of the interaction • no quantitative data —> only qualitative dynamics lybilaB ^» systems biology laboratory Šafránek et al. Formal Biochemical Space 8 Entity Declaration by Example ENTITY ID: KaiC ENTITY NAME: circadian clock protein kinase KaiC STATES: LOCATIONS: cyt CLASSIFICATION: enzyme DESCRIPTION: Monomer component representing a core component of the circadian clock system LINKS: uniprot::Q79PF4, kegg::K08482, ncbi::AAM82686 ORGANISM: SYNPCC7942{Synpcc7942_1216} NOTES: COMPOSITION: S T sybilaQ ^» systems biology laboratory Šafránek et al. Formal Biochemical Space Abstract Entity Specification Class KaiC.KaiC::cyt Specialized class KaiC(S{u}|T{u}).KaiC::cyt KaiC(S{u}).KaiC::cyt Object KaiC(S{u}|T{u}).KaiC(S{u}|T{p}))::cyt sybilad ^» systems biology laboratory Šafránek et al. Formal Biochemical Space Entity Identifier full composition entity name KaiC(S{u)|T{u|).KaiC(S{u}|T{p}))::cyt \ coexistence partial composition compartment sybilad systems biology laboratory Šafránek et al. Formal Biochemical Space 11 Composition Full composition —»• structure of a complex • KaiBC == KaiC.KaiB • KaiC6 == KaiC.KaiC.KaiC.KaiC.KaiC.KaiC Partial composition —»• inner structure of an entity • KaiC(S{u}|T{p}) • cytb6f(f{-}|bl{n}|bhc{2-}) • ps2(qb{2-}|qa{n}|chl{*}|p680{+}|pheo{-}|oec{4+}|yz{n}) sybilaH systems biology laboratory Šafránek et al. Formal Biochemical Space 12 Nested Entity Identifier another way to specify a class entity KaiC protein \cytosol' . 1 S{p}::KaiC::KaiC6::cyt / \ Serine residue KaiC hexamer (phosphorylated) compartment specification is obligatory sybilaQ ^» systems biology laboratory Šafránek et al. Formal Biochemical Space Examples of Entity Identifiers • KaiC6::cyt • KaiA.KaiA::cyt • ATP::cyt • C03{2-}::liq • KaiC(S{u}|T{p})::cyt • C02::?X ; X = {lum, cell, liq, bub, pps, cyt} lybilaB systems biology laboratory Šafránek et al. Formal Biochemical Space 14 Rules vs. Reactions Reaction KaiC(S{u}|T{u})::cyt + KaiC(S{p}|T{p})::cyt KaiC(S{u}|T{u}).KaiC(S{p}|T{p})::cyt object + object => object Rule KaiC::cyt + KaiC::cyt ^ KaiC.KaiC::cyt class + class class sybilaH systems biology laboratory Šafránek et al. Formal Biochemical Space 15 Stringency of Entity Identifiers • consider the rule: S{p}::KaiC::KaiC6::cyt S{u}::KaiC::KaiC6::cyt • both sides identify the same object in location cyt • it is a complex KaiC6 (assume it has a given well-defined full composition) • which contains at least one KaiC protein • whose partial composition contains S{p} lybilaB ^» systems biology laboratory Šafránek et al. Formal Biochemical Space 16 Translation of Entities to Kappa Assume every entity composition is lexicographically ordered. • agent <— entity name • agent name <— entity name suffixed with a location • interface <— partial composition (at least two internal states are required) • site <— each member entity of partial composition • site name <— name of a member entity • internal state state of the entity • binding State <— assign a generic structure, i.e., linear sybilaQ ^» systems biology laboratory Šafránek et al. Formal Biochemical Space 17 BCSL Rules Expressed in Kappa • left/right side S of a BCS rule is set of entities => expressed as a set E of agents in Kappa • since each entity in S is lexicographically ordered, rules are ensured to be unique (up-to structural equivalence of reaction complexes), • for full compositions ('.' operator) a labeling by bound sites is created (concretisation) => abstract meaning of coexistence is lost lybilaB ^» systems biology laboratory Šafránek et al. Formal Biochemical Space 18 Examples BCS: 2 KaiC(S{p}) =► KaiC(S{p}).KaiC(S{p}) Kappa I KaiC(Sp), KaiC(Sp) KaiC(Sp), KaiC(Sp) BCS: S{p}::KaiC::KaiC6::cyt S{u}::KaiC::KaiC6::cyt Kappa : KaiC(Sp), KaiqS1,!"2), KaiC(S2,T3), KaiC(S3,T4), KaiC(S4,T5), KaiC(S5) -> -)• KaiC(Si), KaiqS1,!"2), KaiC(S2,T3), KaiC(S3,T4), KaiC(S4,T5), KaiC(S5) lybilaB systems biology laboratory Šafránek et al. Formal Biochemical Space 19 Case Study: Synechocystis Metabolism • over 1000 entities (objects) and over 500 rules • entities concrete since there is no combinatorial explosion (rules are reactions) • two mathematical models are mapped Photosynthesis and Respiration • over 100 entity classes and over 50 rules • compaction is significant mainly for reactions • one (lumped) mathematical model is mapped Cyanobacterial circadian clock • 18 class entities interacting in 18 rules • creates over 500 object entities • two (lumped) mathematical models are mapped Šafránek et al. Formal Biochemical Space 20 Cyanobacteria Circadian Clock BCS kaiA mRNA Šafránek et al. Formal Biochemical Space 21 Conclusions • in the paper: formal syntax and semantics of BCS • implementation: operational semantics in BNGL (then translated to DiVinE) • currently we work on direct SOS to employ CTL model checking directly on BCS • it will allow to study equivalences and reduction directly at the syntactic level of BCS sybilad ^» systems biology laboratory Šafránek et al. Formal Biochemical Space 22 The End Thank You for your attention. sybilaQ systems biology laboratory Šafránek et al. Formal Biochemical Space 23 The Project Team Humboldt University Berlin University of Vienna University of Turku University of Oxford ... SB study programme ( CzechGlobe Centre for Global Climate Change Impacts Studies systems biology laboratory sybilaQ systems biology laboratory Šafránek et al. Formal Biochemical Space