COMP525

Reasoning About Action And Change

Aims

1. Give the student a feel for several formalisms that deal with change
2. Show how logics can be used to specify and verify dynamic systems
3. Give students a deeper knowledge of the semantics of such systems
4. Develop awareness of the usual trade-off between expressivity and complexity of logical languages.

Syllabus

Introduction - logics, proof, verification (1 week)
Linear Time Temporal Logic (LTL) (3 weeks)
Branching Time Temporal Logic (CTL) (2 weeks)
Dynamic logic (PDL) (2 weeks)
Alternating Time Temporal Logic (ATL) (2 weeks)

Recommended Texts

Reading lists are managed at readinglists.liverpool.ac.uk. Click here to access the reading lists for this module.

Learning Outcomes

(LO1) Provide formal specifications, using a logical language, of informal problem descriptions.


(LO2) Verify simple properties of models.


(LO3) Produce simple logical proofs.


(LO4) Understand how temporal logics relate to each other.


(LO5) Understand and use model checkers.


(LO6) Understand and be able to explain and fomulate properties (such as "safety", "fairness" and "liveness") of systems and be able to formulate simple instances of them.


(S1) Numeracy/computational skills - Reason with numbers/mathematical concepts


(S2) Numeracy/computational skills - Problem solving

Learning Strategy

Teaching Method 1 - Lecture
Description:
Attendance Recorded: Not yet decided


Teaching Method 2 - Tutorial
Description:
Attendance Recorded: Not yet decided