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.
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.