Einführung in Model Checking

... on the evaluation page.

... on the evaluation page.

... on the evaluation page.

There was a typo in the translation from LTL to GNBAs. The transition from q₀ has input vector (d₁,...,d_n) and not the vector (a₁,...,a_n).

On February 19 there will be an open discussion in HS 10 starting at 12:00. Please prepare for the second exam before and your open questions will hopefully be answered during this discussion.

... on the evaluation page

There was a typo in the definition of the semantics of until. The forall-quantifier for i was missing.

The slides of lecture 13 now include the channel-system for the nanoPromela graph.

The exam on Jan 28 will be from 13:30 - 14:30. More details are available on the evaluation page.

One part of the lecture on Jan 21 will be a short repetition of topics of your choice. To find out which topics are of most interest, please send me an e-mail with a short description of would you would like to see again until Thursday 1pm. (Send the e-mail to rene._mylastname_@uibk.ac.at or use the anonymous way via the feedback form.)

In the calculation of the size of transition graph of a promela program was a minor mistake in the example. (The local variables have not been considered.) The slides are fixed now.

In the exercises of lecture 10 the ill-formed formula E A g should be replaced by E G g. The slides are updated accordingly.

The slides of lecture 6 now include the full proof that {w | w contains only finitely many A's} is not recognizable by a DBA.

The date of the exam is fixed: Jan 28 in HS A. One can register for the exam from Nov 15 until Jan 14, 16:00.

Since HS 11 seems a little bit too small, from now on the lecture will be in HS C.

Unlike what was said in the lecture, there is no registration for the lecture required! One only has to register for the exam.