- 17.01.2019: the equation called affinity on slide 27 of Lecture 16+17 should read: ert(P, a.t+t’) = ert(P,0) + wp(P,t) + wp(P,t’). That is, the last two occurrences of ert on the right-hand side of the equations should be both replaced by wp.
- 18.12.2018: the problems with RWTH Online seem to be resolved, so please register for the exam as soon as possible. In case of any problems, let us know.
- 12.12.2018: on slide 29 of lecture 14+15, there was a typo in the bracketing of the progress condition. A new version of the notes of lecture 14+15 has been updated.
- 11.12.2018: the last lectures in 2018 take place on December 18 and 20. The last lecture of this course takes place January 10, 2019.
- 27.11.2018: on the last slide of Lecture #11 the statement cwp(P, (f, 1)) = (Q,f) should read cwp(P, (f,1)) = wp(Q,f). We also updated exercise sheet 6 accordingly.
- 24.11.2018: the exercise class on Friday 7.12 will take place during the lecture slot on Thursday 6.12. So instead of a lecture, there will be an exercise class on 6.12 and no exercise class on 7.12.
- 24.11.2018: on slide 21 of lecture 8+9 the following premise has to be added: I is a wp–subinvariant of while(G) P with respect to f.
- 07.11.2018: Besides the plain and annotated slides, for some of the lectures additional material is made available. This material is meant as background material. Its usage is recommended but optional. Some of the notations in this material are slightly different from the lecture, and some issues are treated in a more general, extensive manner.
- 05.11.2018: Please notice that the lecture on Thursday, 08.11.2018, and the exercise class on Friday, 09.11.2018, have been swapped. The exercise class will take place on Thursday in room 5055 and the lecture will take place on Friday in room 5056, respectively. Furthermore, notice that this means that the third exercise sheet is due on Thursday, 08.11.2018.
- 02.11.2018: If you hand in your exercises via L2P, we kindly ask you to hand in a single PDF file. Moreover, please do not handing in scanned pages. If you cannot hand in right before the lecture, it is possible to hand in exercises at our chair.
- 25.10.2018: a more precise definition of periodic states (Lecture 3, slide 27) is given here:
- 20.10.2018: an update of the slides of Lecture 3 has been uploaded.
- 19.10.2018: Please notice that you have to search for “probabilistic programming” or “probabilistische Programmierung” among all courses in RWTH Online to register for the course.
- 11.10.2018: To get a better idea about the kind of exercises you will encounter throughout the course, you can find some old exercises on our old website.
- 09.10.2018: The first three lectures take place on Thu October 11, Thu October 18 and Fri October 19.
- 11.09.2018: Please notice that (despite different information in RWTHonline) students will be awarded 6 ECTS credits for the lecture after passing the final exam.
|Lecture||Tue||14:30 – 16:00||5052||23.10||Katoen|
|Thu||14:30 – 16:00||5055||11.10||Katoen|
|Exercise||Fri||14:30 – 16:00||5056||26.10||Matheja|
Motivation and background
Probabilistic programs support random choices like “execute program P with probability 1/3 and program Q with probability 2/3″. Probabilistic programs are typically normal–looking sequential programs describing posterior probability distributions. Describing randomized algorithms has been the classical application of these programs. Applications in biology, machine learning, quantum computing, security, and so on, have led to a rapidly growing interest in probabilistic programs in the last decade. For almost all programming languages, such as C, C#, Prolog, Haskell, Scala, LISP, a probabilistic variant does exist; and even a variant of Microsoft’s Excel has been developed, see the probabilistic-programming.org.
Most of these languages feature, in addition to sampling from probability distributions, the ability to condition values of variables in a program. Conditioning allows for adding information about observed events into the program that may influence the posterior distribution. It is one of the key features in Bayesian networks that rely on Bayes’ rule as the basis for updating information. It is this feature that distinguishes modern probabilistic programming languages from those in the early days describing randomized algorithms.
What is special about probabilistic programs? Although probabilistic programs are normal–looking programs, reasoning about their correctness is intricate. They do not generate a single output but a distribution over outputs. The key property of program termination exemplifies this. Whereas a classical program terminates or not, this is no longer true for probabilistic programs. They can diverge, but this may happen with probability zero. That is, even if programs terminate with probability one, they may have non-terminating runs! In addition, in contrast to classical programs that either do not terminate at all or terminate in finitely many steps, a probabilistic program may take infinitely many steps on average to terminate, even if its termination probability is one.
Establishing correctness of probabilistic programs needs—even more so than ordinary programs—formal reasoning.
- What do probabilistic programs mean? Exactly.
- What does it mean for a program to not terminate with some likelihood?
- How to analyze that a probabilistic program does what it is supposed to do?
- How to prove that a probabilistic program is (more) efficient?
- What are Bayesian networks and how are they related to probabilistic programs?
- To achieve a certificate to this course or to be admitted to the final exam, at least half of the exercises has to be reasonably dealt.
- The exercise sheets will be issued weekly. The first exercise sheet will be made available here on October 19, 2018.
|3||Oct 19||Markov chains||PP2018_Lec3||Notes3|
|4||Oct 23||Probabilistic GCL||PP2018_Lec4||Notes4||ex02||pGCL|
|5||Oct 25||Domain theory||PP2018_Lec5||Notes5|
|6||Oct 30||Weakest preconditions||PP2018_Lec6||Notes6||ex03||dijkstra_wp|
|7||Nov 6||Probabilistic weakest preconditions||PP2018_Lec7||Notes7+8A||ex04||probabilistic-wp|
|8||Nov 9||Loop invariants (1)||PP2018_Lec8+9||loop-invariants|
|9||Nov 13||Loop invariants (2)||Notes8B+9||ex05|
|11||Nov 20||Conditioning with weakest preconditions||PP2018_Lec11||Notes11||conditioning|
|12||Nov 27||Hardness of computing weakest preconditions||PP2018_Lec12||Notes12||ex07|
|13||Nov 29||Hardness of almost-sure termination||PP2018_Lec13||Notes13|
|14||Dec 4||Proving almost-sure termination||PP2018_Lec14||ex08||proving-termination|
|16||Dec 13||Runtime Analysis||PP2018_Lec16+17|
|17||Dec 18||Runtime Analysis||Notes16+17|
|18||Jan 8||Bayesian networks||PP2018_Lec18||Notes18||ex09|
|19||Jan 10||Analysing Bayesian networks||PP2018_Lec19||Notes19|
- Written exam on: February 25, 2019 (10:00-12:00, in AH IV (2354|030)) and March 27, 2019 (10:00-12:00)
- The lecture will be given in English. All course material will be in English.
- The students will be awarded 6 ECTS credits for the lecture after passing the final exam. The current indication in RWTHOnline is (unfortunately) incorrect.
The course is based several research papers and material from several books:
- Annabelle McIver and Carroll Morgan — Abstraction, Refinement and Proof for Probabilistic Systems, Springer, 2005.
- Noah Goodman and Andreas Stuhlmüller (electronic) — The Design and Implementation of Probabilistic Programming Languages, 2018.