Temporal Logics see 7 above, 4th example: the formula cUd is true in the last node as well.
CTL Model-Checking see 3 a)-f): the partial formulas are checked in the Kripke structure for all states not merely for x0.
===== Lecture Notes =====
Mr. Matthias Lebok (student) has provided his lecture notes as a pdf file which is available for download (no responsibility is taken for the correctness of it). Please report any mistakes you may find in the forum. (pdf)
Errata: We will provide a revised version at the end of the semester.
===== Exercise =====
The exercise will take place Thursdays from 10:00am to 11:30am.
=== Estimated Dates: ===
2007-06-14 (room 2323, Chair of Computer Science 11)
2007-06-28 (room 2323, Chair of Computer Science 11)
=== Übungsschein ===
In order to achieve the Übungsschein
you may be absent for max. one exercise session with attestation,
you must present a solution with your group at least one time
and you must pass the exam (estimatedly on 2007-07-10 10:00am-11:00am).