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 ECXφ, ECφUΨ and ECGφ?
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?