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:


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


Read §§1–3 of this tutorial article.


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