FDD3006: Temporal Logic

Course Description

Topic

Temporal logic concerns the problem of expressing and proving interesting properties of time-dependent systems. Many variants of temporal logic have been studied over the past 20 years or so, involving discrete or continuous time, interval or point-based reasoning, and explicit or implicit time or probabilities. In this short course we focus on propositional linear time temporal logic, LTL, one of the most basic and well-studied temporal logics. LTL is used widely in computer science and software engineering for program specification and verification, and in the course we cover its main theoretical underpinnings in terms of axiomatizability, expressiveness, and decidability.

Aims

The course is intended to give students a compact, but thorough, introduction to the topic of temporal logic and its theoretical foundations. The main audience is graduate and postgraduate students in computer science, and engineering students with a good background in logic and discrete structures. Upon completion of the course, the student will develop a working understanding of the main mathematical tools and techniques in the area of temporal logic and be able to use these techniques in other contexts related to temporal logic, and in the critical examination of published work in the area.

Course Structure

The course consists of 6 3-hour sessions of which 2 are devoted to lectures and 1 to exercises. We plan 2 sessions per week over three weeks.

Program

Lecture 1	Introduction to temporal logic, slides
	What is temporal logic about? Examples: Mutex, the alternating bit protocol, agents and concurrency How is temporal logic used: Proofs and model checking
Lecture 2	Models and model checking , slides
	Syntax and semantics of propositional Linear Temporal Logic (LTL). Exercises Kripke models for LTL. Model-checking LTL properties Decidability of validity and the small model property for LTL.
Lecture 3	Proof system, slides
	A Hilbert-style proof system for LTL. The meaning of individual axioms: modal correspondence by the assignment method Completeness of the proof system by a tableau construction Prospective addition: A sequent-style proof system. Cut- and invariant-freeness.
Lecture 4	Past LTL: Separation and expressive completeness, slides
	LTL with operators for the past (PLTL) . Gabbay's separation theorem. Eliminating the past operators. Expressive completeness of PLTL.
Lecture 5	Past LTL: Classification of the definable properties and canonical forms, slides
	LTL models as omega-languages Safety, guarantee and obligation, persistence, recurrence and reactivity Closedness, complementarity and inclusion between the classes The safety-liveness classification Closedness, complementarity and inclusion in the language of PLTL Canonical forms with proofs using the separation theorem
Lecture 6	Branching time, slides
	Okhamist and Priorean logics: LTL, CTL and CTL* Model checking for CTL and CTL* Embedding in the modal mu-calculus Other program logics: PDL mu-PDL, FLC

Lecturers

• Mads Dam, CSC/TCS, course responsible
• Dimitar Guelev, Inst. of Mathematics and Informatics, Sofia, Bulgaria

Course Literature

Lecture notes will be made available

Schedule

All lecturers at CSC, Lindstedtsvägen 3, 5th floor

Lecture 1: Monday Aug 24 9.15-12, room 1537

Lecture 2: Thursday 27 Aug 9.15-12, room 1537

Lecture 3: Monday 31 Aug 9.15-12, room 1537

Lecture 4, Thursday 3 Sept 9.15-12, room 1537

Lecture 5, Monday 7 Sept 9.15-12, room 1535 (!)

Lecture 6, Thursday 10 Sept 9.15-12, room 1535

Requirements

• Active participation at lectures. Attendance is compulsory. Please notify the course instructor if you are not able to attend a lecture.
• Submission of solutions to the home assignments.

Grading

The course is awarded 4 ECTS points. Grading is pass/fail, based on the home assignments.