TU Wien:Computer Aided Verification VU (Weißenbacher)/Exam questions ss 2018

Task 1: CTL-Modelchecking on a Kripkestructure. Formula had to be transformed into some kind of normal form before using only quantifiers EU and EG. Addiotionall a parse tree had to be drawn for the formula.

Task 2: Some statements to formalize in CTL*.

Task 3: Give a propositional-encoding for the lasso-formula (like in the lecture on BMC) of the release operator.

Task 4: Single choice (true/false) answers to different questions about all kinds of subjects of the Lecture.