Module Details
The information contained in this module specification was correct at the time of publication but may be subject to change, either during the session because of unforeseen circumstances, or following review of the module at the end of the session. Queries about the module should be directed to the member of staff with responsibility for the module.
Title REASONING ABOUT ACTION AND CHANGE
Code COMP525
Coordinator Dr CL Dixon
Computer Science
Cldixon@liverpool.ac.uk
Year CATS Level Semester CATS Value
Session 2019-20 Level 7 FHEQ Second Semester 15

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.


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

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)

Teaching and Learning Strategies

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

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

Teaching Schedule
  Lectures Seminars Tutorials Lab Practicals Fieldwork Placement Other TOTAL
Study Hours 30

   10

       40
Timetable (if known)              
Private Study 110
TOTAL HOURS 150

Assessment
EXAM Duration Timing
(Semester)		 % of
final
mark		 Resit/resubmission
opportunity		 Penalty for late
submission		 Notes
Written Exam There is a resit opportunity. Standard UoL penalty applies for late submission. This is an anonymous assessment. Assessment Schedule (When) :Semester 2  150 minutes.    75       
CONTINUOUS Duration Timing
(Semester)		 % of
final
mark		 Resit/resubmission
opportunity		 Penalty for late
submission		 Notes
Assessment 1 There is a resit opportunity. Standard UoL penalty applies for late submission. This is not an anonymous assessment. Assessment Schedule (When) :Semester 2  36 hours for all CAs    12       
Assessment 2 There is a resit opportunity. Standard UoL penalty applies for late submission. This is not an anonymous assessment. Assessment Schedule (When) :Semester 2  36 hours for all CAs    12       

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