PathwayLogic通路邏輯.ppt

1、Pathway Logic,Symbolic Analysis of Biological Signaling,Presented by Geoffrey,Introduction,Tremendous growth of genomic sequence information combined with technological advances in the analysis of gene expression has revolutionized research in biology and biomedicine Investigation of signaling and m

2、etabolic pathways would benefit greatly from the use of predictive models Although these pathways are complex, fundamental concepts that stemmed from contemporary research indicates that they are also amenable to analysis via computational methods. E.g. most signaling pathways involved hierarchical

3、assembly in space and time of multi-protein complexes that regulate the flow of information via stimulation or inhibition,Introduction,Various models have been proposed that incorporates quantitative information such as rate and/or concentration information However they are limited due to the diffic

4、ulty in obtaining the relevant parameters e.g. Michaelis constant etc. as well as stochastic features of signaling molecules Hence another way to look at such pathways is by the logic of signal, e.g. use of -calculus to represent and forward simulate signaling pathway In this paper, we will look at

5、the development of logical models based on the application of formal methods tools to mammalian signaling pathways,Levels of Abstraction,Continuous Abstraction Involves continuous mathematics such as differential equations and are analyzed using sophisticated numerical computational packages However

6、 the complexity of biological processes limits its accuracy and effective description Discrete Abstraction Natural processes are described by purely symbolic expressions Applicable to less predictable phenomena such as biological signaling processes (as we shall see later on,Pathway Logic,Pathway Lo

7、gic an algebraic structure enabling the symbolic analysis of biological signaling pathways It uses rewriting theories to formalize the informal models that biologists use to describe processes Advantages of using Pathway Logic: Can include both facts and principles relating and categorizing data ele

8、ments and processes Allows data to be interpreted, combined and queried in the context of biological knowledge Allows models with various levels of details Dynamically generate pathways using search and model-checking Transformation to Petri nets for analysis and visualization Roadmap views of dynam

9、ically generated pathways Pathway logic algebra can be written in the Maude executable specification language,Pathway Logic Example,As an example, we will consider a major receptor-mediated pathway in mammalian cells, focusing on the Epidermal Growth Factor Receptor,Fragment of the mammalian EGFR sy

10、stem illustrating the activation of a downstream mitogenic signaling pathway involving the gene for the autocrine EGRF ligand TGFa,Biological Sorts and Elements,The basic declaration of types in Pathway Logic (or Maude) is by using the keyword sorts and subsorts Constants and operators are defined u

11、sing the keyword ops,sorts Protein Chemical Thing . subsorts Protein Chemical Protein . ops Ca+ : - Chemical,EGRF, EGF, PIP3, Pdk1, PKCe are operations that maps from empty to the Protein sort, indicating that they are constants of Protein,Thing is a sort that encompasses Protein and Chemical, somet

12、hing like a super class,Protein Modification,Pathway Logic allows a comprehensive algebra of protein modification. The example below shows a small part of its declaration and specification in Maude,sorts Modification ModSet . subsort Modification Modification . op none : - ModSet . op _ _ : ModSet M

13、odSet - ModSet assoc comm id: none . op _-_ : Protein ModSet - Protein right id: none,This line denotes a list of modification sets that has elements that are associative, commutative and has none as its identity element,Sets of modifications are applied to proteins using the operator _-_ for exampl

14、e EGRF act represents the activated form of EGRF,Protein Association,Signaling proteins commonly associate to form functional complexes. This is represented using Maude by the following specification code,sort Complex . subsort Complex Complex comm,Hence multi-protein complexes can be specified from

15、 proteins and other things by using the “ : ” operator And example would be the inhibitory complex (IqGap1 : (Ecadherin : bCatenin,Protein Compartmentalization,In eukaryotic cells (i.e. cells with nucleus) proteins and other molecules exist in complex mixtures that are compartmentalized. They are re

16、presented algebraically by the following declarations,Sorts Soup Enclosure MemType . Subsort Thing Soup . Op _ _ : Soup Soup - Soup assoc comm id: empty . Ops CM NM : - MemType . Op _|_ : MemType Soup Soup - Enclosure,The type of membrane,Contents of the membrane,Contents of the membrane,Protein Com

17、partmentalization,An enclosure has its own membrane part and internal, each with its own constituent soup For example,CM | cm:Soup PIP3 Pdk1 - act cyto:Soup PKCe,This represents a cell containing the chemical PIP3 and the activated form of Pdk1 in the cell membrane and PKCe in the interior (or cytop

18、lasm) cm:Soup and cyto:Soup are variables that are declared on the fly of sort Soup,Analysis Techniques,Given a formal symbolic model of the networks, several kinds of analyses can be carried out Static Analysis Forward and Backward Search Explicit State Model Checking Meta-analysis Static analysis

19、allows one to examine the structure of the model and to understand how the elements are related and organized by just looking at the model itself It also provides a means to check for inconsistencies or ill-formed declaration and also to look for missing information,The Dynamics of Pathway Logic Bio

20、chemical Events,To model biochemical events such as signaling processes, we use the dynamic part of a rewrite theory, or rewrite rules, to express such reactions To express the following rule “Activated Erk1 is rapidly translocated to the nucleus where it is functionally sequestered and can regulate

21、 the activity of nuclear proteins including transcription factors”, we have the following rule in Maude,rl410.Erk1/2.to.nuc: CM | cm:Soup cyto:Soup Erk1-act NM | nm:Soup nuc:Soup = CM | cm:Soup cyto:Soup NM | nm:Soup nuc:Soup Erk1-act . rl438.Erk.act.Elk: ?Erk1/2-act Elk1 = ?Erk1/2-act Elk1-act,The

22、Dynamics of Pathway Logic Biochemical Events,As another example, “In the presence of PIP3, activated Pdk1 recruits PKCe from the cytoplasm to the cell membrane and activates it,Rl757.PIP3.Pdk1.act.PKCe: CM | cm:Soup PIP3 Pdk1-act cyto:Soup PKCe = CM | cm:Soup PIP3 Pdk1-act PKCe-act cyto:Soup metadat

23、a “cite = 21961415”,The metadata is just an optional tag that cites the justification of the rule using the MedLine database Unique Identifier,Dynamic Analysis,Hence given the cell declarations and the rewriting rules, we can analyze networks by executing the rewriting rules to obtain cell states In

24、 Maude there are two rewriting strategies the normal top down strategy by means of the command “rewrite” and the command “frewrite” which means fair rewrite. The second one is better as it ensures that no laws are left out in the execution We can also find all the possible outcomes using the command

25、 “search,Dynamic Analysis,Hence considering the PKC network,op q14 :- Dish . eq q14 = PD(Ca+ CM | PIP2 PI3Ka-act PLCb1-act Pten-act Erk1 Pdk1 PKCa PKCe),Using the rewrite and frewrite commands will give,rewrite q14 . result Dish: PD(CM | Ca+ DAG IP3 PI3Ka-act PLCb1-act Pten-act Erk1 Pdk1 PKCa-act PK

26、Ce-act NM | empty empty ) frewrite q14 . Result Dish: PD(CM | Ca+ DAG IP3 PI3Ka-act PLCb1-act Pten-act Pdk1-act Erk1 PKCa-act PKCe-act NM | empty empty,Dynamic Analysis,Using the search command,search q14 =! D:Dish . . Solution 3 (state 23) D:Dish - PD(CM | Ca+ DAG IP3 PI3Ka-act PLCb1-act Pten-act P

27、dk1-act PKCe-act PKCa-act NM | empty Erk1-act,Path Graph of the PKCe network,Search till termination,Model Checking,One of the capabilities of using Pathway Logic and Maude system is Model Checking LTL (Linear Temporal Logic) formulas can be used to assert whether or not a state is reachable (This h

28、as uses in biomedicine to find out whether or not, targeting a specific enzyme will produce side effects,subsort Dish Prop . eq PD(out:Soup CM | cm:Soup cyto:Soup NM | nm:Soup NM | nm:Soup cJun-act cFos-act) |= prop1 = true . red q1 |= prop1,Meta Analysis,There is a variety of metadata associated wi

29、th the executable model of a signaling network. This includes information justifying or qualifying a rule and also ordering information, i.e. allows us to reason about the models themselves These form of analyses can be used to answer simples questions such as “What are the rule labels?” or “What co

30、nstants of the sort Protein have been declared?” These questions are used to query about the model structure and content,Graphical Representation,Ultimately, Maude is still a text based tool which may not be suitable for biologists to study and analyze One way to view Pathway Logic is to use BioNet viewer, which is an applet written by the authors to view the pathways In the model, ovals represent the components (proteins, chemicals) with blue ovals representing the initial states while white ovals r