For the midterm exam the students should:

- know the notion of a formal method and scope of applicability of formal methods

- know the propositional and first order logics, be able to define pre- and post-conditions using them

- know the notions of completeness and soundness

- know the modal logic; notion of Kripke structure; be able to determine if a certain Kripke structure satisfies a modal logic formula

- know the syntax and semantics of LTL, CTL and CTL*

- know the differences in expressiveness of LTL, CTL and CTL*

- understand definition of properties in LTL, CTL and CTL*

- know the gist of CTL model checking algorithms (for AFp, EFp, A( p U q ), E(p U q), AGp, EGp )

- be able to determine if a certain Kripke structure satisfies a temporal logic formula (CTL, LTL)

- know the notion of a strongly connected component and its importance for model checking AGp and EGp