give the student a feel for several formalisms that deal with change
show how logics can be used to specify and verify dynamic systems
give students a deeper knowledge of the semantics of such systems
develop awareness of the usual trade-off between expressivity and complexity of logical languages
make students aware of some standard problems of modelling change in AI-formalisms
Introduction - logics, proof, verification (1 week)2
Linear Time Temporal Logic (LTL) (3 weeks).3
Branching Time Temporal Logic (CTL) (2 weeks)4
Dynamic logic (PDL) (2 weeks).5
Modelling change in AI (2 weeks)
Logic in Computer Science Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, Second Edition, Cambridge University Press, 2004.
Model Checking, Edmund M. Clarke, Orna Grumberg and Doron A Peled, The MIT Press, 1999.
Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems, R. Reiter, MIT Press, 2001.
Knowledge Representation and Reasoning, R. Brachman and H. Levesque, Morgan Kaufmann, Elsevier, 2004.
Dynamic Logic, D. Harel, D. Kozon and J. Tiuryn, MIT Press, 2000.
Provide formal specifications, using a logical language, of informal problem descriptions.
Verify properties of models.
Produce simple logical proofs.
Understand how temporal logics relate to each other.
Understand and use model checkers.
Understand and be able to explain and formulate properties (such as "safety", "fairness" and "liveness") of a given system
Have an awareness of techniques to guarantee "preservation" when reasoning about change.
Formal Lectures: Students will be expected to attend three hours of formal lectures in a typical week plus one hour supervised tutorial.
Private study: In a typical week students will be expected to devote six hours of unsupervised time to private study. The time allowed per week for private study will typically include three hours of time for reflection and consideration of lecture material and background reading, and three hours for completion of practical exercises.