Pruefer: Tadeusz Litak
Beisitzer: Christopher Rauch

• What are the syntax of LTL and CTL?
• We have E and A in CTL. How is it in LTL?
• So, is CTL more expressive than LTL?
• Give some examples of formulas expressible only in LTL and only in CTL?

• How does model checking in CTL work?
• Can we check fairness constraints with this algorithm?
• When checking for fairness, do we have to check for E_CXφ, E_CφUΨ and E_CGφ?
• Which fixpoint theorem did we use?

• Can you give the partial correctness Hoare rule for WHILE?
• How do we have to extend it for total correctness?
• What is more suited for total correctness than Hoare rules?
• Can you give the definition of wp(WHILE,B)?

• Now to separation logic: Does (A*T)ΛB ↔ (A*(A-*B)) always hold?
• Can you give small axioms for our dynamic programming constructs?
• Which rule did we use to derive the global rules?
• Can you give a total axiom and its derivation?