Assignment source

22 February 2010

I have put online the LaTeX source for the assignment sheet. This is only for completeness, and possible LaTeX interest — it doesn’t have any clues hidden inside it.


Absence

22 February 2010

My apologies, but I am ill and so shall not be able to give the MLCSB lecture today.

In addition, I shall be giving a seminar in Birmingham at the end of the week and so there is no lecture on Thursday either.

The next MLCSB lecture is on Monday 1 March, and will be about stochastic simulation and the Gillespie algorithm.


Typesetting Petri Nets

18 February 2010

Donal asked about typesetting Petri nets. I’m using the LaTeX style PGF/TikZ; this renders things well, and plays nicely with the beamer class for creating slides. These are ridiculously extensive packages, both written by Till Tantau — I cannot imagine how he finds the time.

TikZ works with moderately high-level descriptions of diagrams: for Petri nets, once the location of places and transitions are set it will draw the links between them, according to suitable styling instructions. It also works entirely within TeX, which is a help for portability. (We’ll leave aside the issue of whether trigonometric computation is a sensible task to attempt in a language designed for text preparation.)

Browse the gallery of TikZ examples to see what can be done. There are even PDF animations, like this one of set intersection (source code).

I have no plans to animate my Petri nets, although I’m sure it could be done.

Chris said he had experience with dot2tex, which I have not used.

Any other suggestions on good ways to draw Petri nets?


Lecture 11: Markov Chains and Stochastic Logics

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:

Homework

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?


Lecture 10: Stochastic Petri Nets and Markov Chains

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.

Link: Slides

Homework

Read §§1–3 of this tutorial article.

Assignment

The first assignment is now out. See the coursework web page for more information.


Lecture 9: Continuous time

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)

Homework

Read the following short articles for Thursday.


Lecture 8: Mix, match and use temporal logics

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.

Link: Slides


Lecture 7: From LTL and CTL to CTL*

2 February 2010

Review and comparison of the syntax and semantics of temporal logics LTL and CTL. Distinction between the direct observability of individual runs, and the assessment of alternative possibilities in branching-time logics like CTL. Valuation of CTL formulae on specific transition systems. Distinct expressiveness of LTL and CTL: example to show AF AG is not AFG.

Link: Slides (with CTL valuation table corrected)

Reading

Two items to read for Thursday:

The first of these is an invited conference talk, giving an overview of some work on applying model-checking to problems in systems biology. The second is a more detailed article on the material.


Lecture 6: Branching Time and CTL

28 January 2010

Update: Revised reference to Fages and Rizk time series paper — see below.

The slides for this lecture review Linear Temporal Logic (LTL), with several examples of LTL formulae for expressing properties of Petri Net behaviour.

Boardwork then gave the expansion from linear time to branching time, the syntax for CTL formulae, and some small discussion of their interpretation.

The final slide gives some further reading, reproduced below. All articles are linked to web pages where you should be able to download copies: you may be asked to log in with the EASE authentication service along the way.

Read the rest of this entry »


Lecture 5: Linear Temporal Logic

25 January 2010

The slides for this lecture review the notions of labelled transition systems, runs and traces, and give examples of the expansion of Petri net behaviour into labelled transition systems.

Boardwork then gave definitions of LTL formula, their meaning, and some small examples of application to LTS runs and Petri net behaviours.

Heiner et al. discuss how even finite reachability graphs for Petri nets may blow up very fast (§4(5)). However, they then jump straight to branching-time with CTL.

Huth and Ryan present the syntax and semantics of LTL (§3(2)) as well as some motivation on model checking.

The SPIN tool is based on LTL model checking.