The Pathway Logic Formal Modeling System: Diverse views of a formal representation of signal transduction.

摘要

The core of the Pathway Logic signal transduction model (STM) is a theory in the rewriting logic language Maude. This theory provides a language for representing the signaling state of a cell and its components, and rewrite rules representing possible signaling events. Used as a theory in rewriting logic, statements about signal propagation can be proved. The theory can also be viewed as a database that can be queried, for example, to find the events in which a given protein might participate or to retrieve all signaling events (rules) of a given type. Given a representation of a cell state, an executable model can be derived from the theory. This model can be executed to observe a possible behavior, or model checked to study properties of signal propagation pathways. Finally, the theory can be viewed as term in the meta-theory. Using reflection, the theory can be mapped to terms in other formalisms, to access additional reasoning tools; to annotated grapical representations for visualization; or to an external representation such as JSON, SBML or BIOPAX for sharing with other formal systems. The talk will begin with a perspective on formal modeling. We will then discuss identification and representation of elements of a theory of signal transduction motivated by experimental evidence. Finally we show how the views of the resulting theory are used in practice and how the ideas generalize to modeling other cellular processes such as glycosylation and immune system.