We show how the non-monotonic nature of common-sense reasoning can be formalised by circumscription. Various forms of circumscription are discussed. A new form of circumscription, namely naive circumscription, is introduced ...

These tutorial notes contain an introduction to the logical theory and computational aspects of computer aided verification of finite state reactive systems with linear and branching temporal logic model checking. As a ...