Modal Logic for Computer Scientists

Start: Tue April 8th

A course by Lutz Schröder and Till Mossakowski at the Universität Bremen 2008.

03-05-H-604.51
Category V
Prerequisites: content of 600.01, 600.02, 601.01, 601.02, 604.02
ECTS: 6
Monday 13:00 - 15:00 MZH 7250,
Tuesday 13:00 - 15:00 MZH 7220

Modal logic extends the familiar logical operators with so-called modal operators that express that a formula holds in a certain way, e.g. 'necessarily', 'possibly', 'probably', 'as agent X knows/believes', 'forever', 'somewhere' etc. Although originated largely in philosophy, modal logics play an increasing role in computer science e.g. as logics of time, space, computation, knowledge, obligation, or permission, appearing in such diverse fields as KI, verification of parallel programs, and ontology languages for the semantic web. This course will deal with foundations and applications of modal and temporal logic, following the book

M. R. Huth and M. D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004 (2nd edition) Part of the course will consist of practical exercises with model checkers, in particular, the NuSMV model checker.

Further literature:

• Patrick Blackburn, Maarten de Rijke and Yde Venema, Modal Logic, Cambridge University Press, 2001.
• Sally Popkorn, First Steps in Modal Logic, Cambridge University Press, 1994
• B. Chellas, Modal Logic, Cambridge University Press, 1980

Exercises

• Exercise sheet 1 (due: 28th April)
• Exercise sheet 2 (due: 12th May)
• Exercise sheet 3 (due: 23rd June)