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.
Assignment source
22 February 2010
Comments Off on Assignment source | 
Coursework | 
Permalink
Posted by Ian Stark
Absence
22 February 2010My 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.
Comments Off on Absence | Announcements | Permalink
Posted by Ian Stark
Typesetting Petri Nets
18 February 2010Donal 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?
1 Comment | Uncategorized | Tagged: beamer, LaTeX, Petri Nets, tikz | Permalink
Posted by Ian Stark
Lecture 11: Markov Chains and Stochastic Logics
18 February 2010Small 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:
- Marta Kwiatkowska, Gethin Norman, and David Parker. Probabilistic model checking for systems biology. In Symbolic Systems Biology: Theory and Methods. Jones and Bartlett, 2010. To appear.
Homework
Read the remainder of the Kwiatkowska et al. tutorial, §§4–6.
Also, recall this short report:
- Lucas Laursen. Computational biology: Biological logic. Nature 462:408–410, 2009.
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?
Comments Off on Lecture 11: Markov Chains and Stochastic Logics | Lecture Log | Tagged: CSL, CTL, markov chains, model checking, probabilistic, stochastic | Permalink
Posted by Ian Stark
Lecture 10: Stochastic Petri Nets and Markov Chains
11 February 2010Introducing 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.
- Marta Kwiatkowska, Gethin Norman, and David Parker. Probabilistic model checking for systems biology. In Symbolic Systems Biology: Theory and Methods. Jones and Bartlett, 2010. To appear.
Assignment
The first assignment is now out. See the coursework web page for more information.
Comments Off on Lecture 10: Stochastic Petri Nets and Markov Chains | Lecture Log | Tagged: markov chains, stochastic | Permalink
Posted by Ian Stark
Lecture 9: Continuous time
8 February 2010Note: 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.
- Lucas Laursen. Computational biology: Biological logic. Nature 462:408–410, 2009.
- Jasmin Fisher and Thomas A Henzinger. Executable cell biology Nature Biotechnology 25:1239–1249, 2007.
- Nathalie Chabrier and François Fages. Symbolic model checking of biochemical networks. In Computational Methods in Systems Biology, Proceedings of the First International Workshop, CMSB 2003. Lecture Notes in Computer Science 2602, pages 149–162. Springer-Verlag, 2003.
Comments Off on Lecture 9: Continuous time | Lecture Log | Tagged: model checking, Petri Nets, stochastic | Permalink
Posted by Ian Stark
Lecture 8: Mix, match and use temporal logics
6 February 2010Revisit 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
1 Comment | Lecture Log | Tagged: CTL, LTL, model checking | Permalink
Posted by Ian Stark
Lecture 7: From LTL and CTL to CTL*
2 February 2010Review 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:
- H. de Jong. Qualitative modeling and simulation of bacterial regulatory networks. In Computational Methods in Systems Biology: Proceedings of the 6th International Conference CMSB 2008, Lecture Notes in Bioinformatics 5307, p. 1. Springer-Verlag, 2008.
- P. T. Monteiro, D. Ropers, R. Mateescu, A. T. Freitas, and H. de Jong. Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics, 24(16):227–233, 2008.
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.
Comments Off on Lecture 7: From LTL and CTL to CTL* | Lecture Log | Tagged: CTL, LTL | Permalink
Posted by Ian Stark