18 March 2010
Working through the following paper:
- Federica Ciocchetta and Maria Luisa Guerriero. Modelling Biological Compartments in Bio-PEPA, in MeCBIC 2008: Proceedings of the Second International Meeting on Membrane Computing and Biologically Inspired Process Calculi. Electronic Notes in Theoretical Computer Science 227:77–95, January 2009.
Adding compartments to BioPEPA: syntax; compositional operational semantics; structured locations including compartments, membranes, and the boundaries between them; appropriate kinetics; sample model of intracellular calcium oscillations.
Please fill out and submit an anonymous feedback questionnaire. Thank you.
16 March 2010
Guest lecture by Stephen Gilmore explaining and demonstrating the BioPEPA tools, principally the Eclipse plugin.
11 March 2010
Background on process algebras / process calculi: what they can be useful for, and various domains where they have been applied. Specific applications to systems biology; and the wide range of process calculi proposed for different aspects of biological systems.
Brief introduction to PEPA and BioPEPA, with reference to Ciocchetta and Hillston (2009).
8 March 2010
Moving from discrete events to continuous flow: semantics of continuous Petri nets; correspondence with chemical reaction equations; deriving ordinary differential equations (ODEs); conservation laws, equilibria, numerical solutions and trajectories through phase space. Relating transition rates for discrete events to reaction rates for continuous flow; dependence on reaction stoichiometry.
Some examples, including derivation of Michaelis-Menten semantics.
Thursday’s lecture will be an introduction to BioPEPA, followed by Stephen Gilmore on Monday.
Read §§6–9 of Heiner et al., and §§1–4 of Ciocchetta and Hillston, on BioPEPA.
This earlier paper by Gilbert and Heiner also explains modelling biological processes with continuous Petri nets.
5 March 2010
More on Gillespie’s algorithm for stochastic simulation, including the remainder of the slides from Gillespie’s invited CMSB talk. Various tau-leaping methods to more efficiently simulate larger systems; concerns about bounding the errors in these approximate techniques. Further approximation with continuous models, still stochastic, and then by deterministic systems of differential equations for even large scales.
This is discussed in Chapter 8 of Wilkinson’s book on stochastic modelling.
You can also read Gillespie’s own papers on this: his original SSA proposal, and a more recent survey of progress since then.
Return of coursework, and discussion of some particular issues.
- Reachability graph for the repressilator model.
- Drawing subnets arising from transition and place invariants.
- Eight minimal place invariants for the ECA synthesis network; invariants for preservation of uridine, saccharide, phosphate and undecaprenyl groups.
- Logical formulae in LTL, CTL and HML: decoding and coding them.
- The until connective denotes that the statement will eventually hold; release may not.
- HML must modality [a]p means that if a happens, p is then true — but it doesn’t say anything about whether a does happen, or is even possible.
Any more questions or answers about the coursework, please post on the comments below.
2 March 2010
Revisiting Kwiatkowska et al. on probabilistic model-checking for systems biology. Moving from models of a single protein to slightly larger populations, still with symbolic model-checking.
The problem of state-space explosion, and the use of simulation. Gillespie’s algorithm for stochastic simulation. I’m using the slides from Gillespie’s invited talk at CMSB 2007 in Edinburgh. So far we have covered the approximation from precise dynamic simulation of all positions and velocities, down to stochastic simulation of populations through modelling only reactive molecular collisions. This gives the exact SSA; next are various tau-leaping methods for efficient approximation.
Wilkinson’s book on stochastic modelling covers the Gillespie algorithm in §§6.2–6.5, with Chapter 8 then going on to deal with approximation strategies.
Links: Slides; Gillespie on Stochastic Chemical Kinetics; All CMSB 2007 talks.
18 February 2010
Small Petri net example in the form of a signal cascade. Extracting from this in turn: a transition system; a DTMC with transition probabilities; and a CTMC with rates. Corresponding refinements of temporal logic: LTL/CTL; PCTL with probabilities; CSL with probabilities and duration. How this extends expressiveness, and how replacing discrete “always” with probabilistic “almost surely” gives results more closely matching intuition.
Probabilistic symbolic model checking and the PRISM tool. Examples from:
Read the remainder of the Kwiatkowska et al. tutorial, §§4–6.
Also, recall this short report:
In the meantime, however, Fisher and her fellow executable-biology enthusiasts have a lot of convincing to do, says Stephen Oliver, a biologist at the University of Cambridge, UK. “Modelling in general is regarded sceptically by many biologists,” he points out.
Do you think this is true? Can you find any evidence for or against?
11 February 2010
Introducing probability to Petri nets through continuous time and transition firing rates. Markov chains, and variations thereon: Discrete Time Markov Chains (DTMC); Markov decision procedures (MDP); Continuous Time Markov Chains (CTMC). How this last one is appropriate to capture the behaviour of a stochastic Petri net. Brief mention of the PRISM probabilistic model checker.
Read §§1–3 of this tutorial article.
The first assignment is now out. See the coursework web page for more information.
8 February 2010
Note: The slides have been revised since the lecture, removing some untruths, adding more about BDDs and exponential distribution, and providing further references.
Symbolic Model Checking: How advanced algorithms test assertions on systems with states than you can imagine possible.
Road Map Review: Shifting between high-level intuitive models and low-level mathematical ones, with multiple choices and analyses.
Continuous Time: Negative exponential distributions and why we use it; starting with Stochastic Petri Nets.
Link: Slides (updated)
Read the following short articles for Thursday.
6 February 2010
Revisit example valuation of CTL formula, now corrected. Further possible logics: Hennessy-Milner, modal μ-calculus, and monadic second-order logic. Presentation of syntax, semantics, and small examples. Relative expressiveness. Mixing and matching modalities and operators for convenience, distinct from expressiveness: CTL- as an example.
Application to specific biological models, as discussed in these articles: Fages and Rizk evaluating LTL formulae over time series data; de Jong et al. on mapping textual descriptions into CTL.