Formal Methods in Systems Biology

From BioNetWiki

Jump to: navigation, search

Contents

[edit]

Course Info

Course number: 15-872(A)

This course is being offered as part of the Joint CMU/Pitt Graduate Computational Biology Track.

This course is cross-listed as: CMU 02-730, Pitt CMPBIO 2045(Arts & Sciences), Pitt MSCBIO 2045 (School of Medicine)

Link to CMU course home page

Instructors
Chris Langmead, WeH 4103 (CMU); cjl at cs.cmu.edu
James Faeder, BST3 (U. Pitt); faeder at pitt.edu
Credits
12
Description
This course will cover advanced methods for modeling and reasoning about the dynamics of biological systems. Emphasis will be placed on emerging techniques that complement those based on differential equations and machine learning. Specific examples include Rule-based modeling, Process Algebras, Petri Nets, Hybrid Systems, as well as well as applications of model checking and type theory. Students will be asked to present and to provide written summaries of recent papers, and to complete a course project of their own design.
Prerequisites
None
Materials
There is no text. All course materials are published manuscripts from the primary literature.
Method of Evaluation
Grading will be based on in-class presentations and a course project.
Schedule
T, TH 1:30 - 2:50 PM; Newell-Simon Hall 3002 (campus map)
Office Hours
By appointment
[edit]

Schedule

Feel free to post your comments on the Talk pages associated with each lecture (click on the link in the Topic column).

Date Topic Presenter Reading Slides/Notes Comments
15 Jan Introduction Faeder Fisher and Henzinger (2007), Regev and Shapiro (2002) (pdf) ppt, pdf
17 Jan Modeler's View of Cell Signaling Faeder Goldstein et al. pdf This paper gives some concrete examples of the intracellular signaling events that I presented more generally in lecture. --JF
22 Jan Modeler's View of Cell Signaling (continued) Faeder Blinov et al. (2006), Kholodenko et al. (1999) pdf
24 Jan Rule-Based Modeling of Cell Signaling Faeder Hlavacek et al. (2006), Danos et al. (2007a) pdf
29 Jan Process Algebras (1) Langmead Regev and Shapiro pdf
31 Jan Process Algebras (2) Langmead pdf
5 Feb Process Algebras (3) Langmead Calder et al pdf
7 Feb Process Algebras (4) Langmead

Brinksma, E. and Hermanns,

pdf
12 Feb Cancelled
14 Feb Model Checking I Ed Clarke pdf
19 Feb Model Checking II Sumit Jha pdf
21 Feb PRISM Langmead
26 Feb Symbolic Model Checking with BDDs Clarke pdf
28 Feb Using SAT Checkers for Model Checking Clarke pdf
4 Mar Model Checking Application: Gene Regulatory Networks Justin Hogg Batt et al. preprint lecture slides
6 Mar Kinetic Monte Carlo Methods Leonard Harris
18 Mar Probabilistic Boolean Network Suvrajit
20 Mar Introduction to Petri Nets Arvind Ramanathan
25 Mar Stochastic Petri Nets Arvind Ramanathan
27 Mar Hybrid Systems (Linear Hybrid Automata) Sumit Kumar Jha Henzinger et al
1 Apr Statistical Model Checking Justin Hogg Younes and Simmons. "Statistical probabilistic model checking with a focus on time-bounded properties." Information and Computation. Sept 2006.
3 Apr Signal Propagation in Nonlinear Stochastic Gene Regulatory Network Suvrajit S.Achimescu and O. Lipan
8 Apr Detailed Balance Jintao Colquhoun et al, Yang et al, Ederer and Gilles
10 Apr A Thermodynamic Approach on DNA looping Jintao L. Saiz and J. Vilar
15 Apr Kappa Calculus Cordelia
17 Apr No Class - Carnival
22 Apr Abstract Interpretation Cordelia Danos et al. 2008
24 Apr No Class - work on projects
29 Apr Project Presentations Justin Arvind, Sumit
1 May Project Presentations Suvrajit Cordelia, Jintao
[edit]

Subject Areas and Papers

[edit]

Definitions

[edit]

Overviews

  • J. Fisher and T. A. Henzinger (2007) Executable Cell Biology. Nat. Biotechnol., 25, 1239-1249. [1]
  • A. Regev and E. Shapiro (2002) Cells as computation. Nature, 419, 343. [2] (pdf)
  • B. Goldstein, J. R. Faeder, and W. S. Hlavacek (2004) Mathematical and computational models of immune-receptor signalling. Nat. Rev. Immunol., 4, 445-456. [3]
[edit]

Rule-Based Modeling of Signal Transduction

  • W. S. Hlavacek, J. R. Faeder, M. L. Blinov, R. G. Posner, M. Hucka, and W. Fontana (2006) Rules for modeling signal-transduction systems. Sci. STKE., 2006, re6. [4]
  • W. S. Hlavacek, J. R. Faeder, M. L. Blinov, A. S. Perelson, B. Goldstein (2003) The complexity of complexes in signal transduction. Biotechnol. Bioeng., 84, 783-794. [5]
  • V. Danos and C. Laneve (2004) Formal Molecular Biology. Theor. Comput. Sci., 325, 69-110. [6]
  • V. Danos, J. Feret, W. Fontana, R. Harmer and J. Krivine (2007) Rule-based modelling of cellular signalling. Lecture Notes in Computer Science 4703, 17-41. [7] (preprint)
  • O. Andrei and H. Kirchner (2007) Rewrite Rules and Strategies for Molecular Graphs. [8]
  • M. Calder, S. Gilmore, J. Hillston, and V. Vyshemirsky (2007) Formal Methods for Biochemical Signalling Pathways. To appear [9]
[edit]

Model Reduction

  • N. M. Borisov, A. S. Chistopolsky, J. R. Faeder, and B. N. Kholodenko. Domain-Oriented Reduction of Rule-Based Network models. Submitted to IET Systems Biology. (preprint) and references therein.
[edit]

Kinetic Monte Carlo

  • D. T. Gillespie (2007) Stochastic simulation of chemical kinetics. Annu. Rev. Phys. Chem. 58 35-55. PMID 17037977.
  • Review of related papers can be found here.
[edit]

Process Algebras

  • Regev, A. and Shapiro, E. (2001) The pi-calculus as an Abstraction for Biomolecular Systems, Modelling in Molecular Biology, G. Ciobanu, G. Rozenberg (Eds.), Springer, pp. 219-266. [10]
  • Brinksma, E. and Hermanns, H. (2001) Process Algebra and Markov Chains, Lecture Notes in Computer Science, 2090 pp. 183-232. [11]
  • Cardelli, L. (2007) A Process Algebra Master Equation, Fourth International Conference on the Quantitative Evaluation of Systems, IEEE Publishing pp 219-224. [12]
  • Cardelli, L. (2006) From Processes to ODEs by Chemistry, [13]
  • Calder, M and Gilmore, S. and Hillston, J. (2005) Automatically deriving ODEs from process algebra models of signalling pathways, Proceedings of CMSB 2005 (Computational Methods in Systems Biology), pp 204-215,[14]
  • Regev, A. and Panina, E.M. and Silverman, W. and Cardelli, L. and Shapiro, E. (2004) BioAmbients: An Abstraction for Biological Compartments, Theoretical Computer Science, Special Issue on Computational Methods in Systems Biology. Volume 325, Issue 1 , 2004, pp. 141-167,[15]
  • Cardelli, L. (2004) Brane Calculi - Interactions of Biological Membranes, Lecture Notes in Computer Science, Vol 3082, Springer, 2005. pp 257-280, [16]
  • Danos, V. and Laneve, C. (2004) Formal Molecular Biology, TCS, 325 [17]
  • Laneve, C. and Tarissan, F. (2007) A simple calculus for proteins and cells, ENTCS, 171:139-54. [18]
  • Romanel, A., Dematte, L, and Priami, C. (2007) The Beta Workbench. Technical Report 03/2007, Centre for Computational and Systems Biology, Microsoft Research and The University of Trento. pdf
[edit]

Abstract Interpretation

  • Vincent Danos, Jerome Feret, Walter Fontana, Jean Krivine (2008) Abstract Interpretation of cellular signalling networks, VMCAI08. [19]
[edit]

Model Checking

  • J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn (2007) Probabilistic model checking of complex biological pathways, Lec. Notes Comput. Sci., 4210, 32-47. [20] (preprint)
  • G. Batt, C. Belta, and R. Weiss (2007) Temporal Logic Analysis of Gene Networks under Parameter Uncertainty, 10th International Workshop on Hybrid Systems: Computation and Control. preprint
  • G. Batt, H. de Jong , J. Geiselmann , and M. Page () Analysis of Genetic Regulatory Networks: A Model-Checking Approach. (preprint)
  • N. Chabrier and F. Fages (2003) Symbolic model checking of biochemical networks. (preprint)
[edit]

Algebraic Model Checking

  • C. Piazza, M. Antoniotti, V. Mysore, A. Policriti, F. Winkler, and B. Mishra (2005) "Algorithmic Algebraic Model Checking I: Challenges from Systems Biology", 17th International Conference on Computer Aided Verification, CAV pp. 5-19 [21]
  • V. Mysore and C. Piazza and B. Mishra (2005) "Algorithmic Algebraic Model Checking II: Decidability of Semi-Algebraic Model Checking and its Applications to Systems Biology", Automated Technology for Verification and Analysis, ATVA, pp. 217-233 [22]
  • V. Mysore and B. Mishra (2006) "Algorithmic Algebraic Model Checking III: Approximate Methods", 7th International Workshop on Verification of Infinite-State Systems, INFINITY 05, pp. 61-77 [23]
  • V. Mysore and B. Mishra (2007) "Algorithmic Algebraic Model Checking IV: Characterization of Metabolic Networks", Algebraic Biology, AB, pp. 61-77 [24]
[edit]

Agent-Based Modeling of Cellular Behavior

  • D. Walker, S. Wood, J. Southgate, M. H. and R. Smallwood, An integrated agent-mathematical model of the effect of intercellular signalling via the epidermal growth factor receptor on cell proliferation, J. Theor. Biol., 242, 774-789. [25]
  • C. Beauchemin, A. Bauer, and A. S. Perelson (2008) Agent-Based Modeling of Host-Pathogen Systems: The Successes and Challenges. (preprint)
[edit]

Boolean Networks

  • Li S, Assmann SM, Albert R (2006) Predicting Essential Components of Signal Transduction Networks: A Dynamic Model of Guard Cell Abscisic Acid Signaling. PLoS Biol 4, e312. [26]
[edit]

Petri Nets

C. Chaouiya (2007) Petri net modelling of biological networks. Brief. Bioinform. 8, 210–219 (2007). [27]

[edit]

State Charts

  • Fisher, J., Piterman, N., Hubbard, E.J., Stern, M.J. & Harel, D. (2005) Computational insights into Caenorhabditis elegans vulval development. Proc. Natl. Acad. Sci. USA 102, 1951–1956. [28]
[edit]

Hybrid Systems

[edit]

Model Checking Tools

  • NuSMV
  • PRISM
  • Linear Hybrid Automata
[edit]

Conferences

Retrieved from "http://bionetgen.org/index.php/Formal_Methods_in_Systems_Biology"
Personal tools