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:
- 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?
Posted by Ian Stark