### News

Apr 30: Solution and results of third exam online...

... on the evaluation page.

Apr 29: 3rd exam is corrected, reviewing Apr 30, 8:00-8:30, 9:00-10:00. Further details

... on the evaluation page.

Feb 28: Solution and results of second exam online...

... on the evaluation page.

Feb 20: Updated slides of lectures 8 and 9 available

There was a typo in the translation from LTL to GNBAs. The transition from q

_{0}has input vector (d_{1},...,d_{n}) and not the vector (a_{1},...,a_{n}).Jan 30: Diskussion opportunity

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.

Jan 30: First exam and results online...

... on the evaluation page

Jan 25: Updated slides of lectures 7 and 8 available

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

**i**was missing.Jan 21: Updated slides of lecture 13 available

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

Jan 15: Time of the exam is now fixed

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

Jan 14: Feedback required

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.)

Jan 10: Updated slides of lecture 4 available

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.

Jan 02: Bugfix of Exercise 10

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.Nov 12: Updated slides of lecture 6 available

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.

Oct 15: Date of the exam

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.

Oct 15: Change of the lecture hall

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

Oct 12: No registration required

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