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-04-19
2007-05-03
2007-05-24
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).
Questions of general interest will be answered in the forum
This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies
RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany