FDD3006 Temporal Logic 4.0 credits

Temporal logik

Offering and execution

Course offering missing for current semester as well as for previous and coming semesters

Course information

Content and learning outcomes

Course contents *

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 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.

Intended learning outcomes *

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 Disposition

No information inserted

Literature and preparations

Specific prerequisites *

No information inserted

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

No information inserted

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale *

P, F

Examination *

    Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

    The examiner may apply another examination format when re-examining individual students.

    Other requirements for final grade *

    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.

    Opportunity to complete the requirements via supplementary examination

    No information inserted

    Opportunity to raise an approved grade via renewed examination

    No information inserted

    Examiner

    Mads Dam

    Ethical approach *

    • All members of a group are responsible for the group's work.
    • In any assessment, every student shall honestly disclose any help received and sources used.
    • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

    Further information

    Course web

    No information inserted

    Offered by

    EECS/Theoretical Computer Science

    Main field of study *

    No information inserted

    Education cycle *

    Third cycle

    Add-on studies

    No information inserted

    Contact

    Mads Dam, e-post: mfd@csc.kth.se, tel: 790 6229

    Postgraduate course

    Postgraduate courses at EECS/Theoretical Computer Science