In: ILLC Master of Logic Series. 2002
Questionnaires appear in many places around us. Their structure can be quite complex. It is therefore beneficial to reason about them automatically. In this thesis I will define questionnaires; identify their structural properties; and demonstrate how formal methods, namely model checking, can assist in checking structural properties of questionnaires. The SMV model checker is used for the model checking.