COMP525

Reasoning About Action and Change

Aims

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

Syllabus

1

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)

Recommended Texts

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.

Learning Outcomes

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.

Learning Strategy

Formal lecture

Supervised practice

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.