DD3006 Temporal logik 4,0 hp

Temporal Logic

  • Utbildningsnivå

    Forskarnivå
  • Huvudområde

  • Betygsskala

    P, F

Det finns inget planerat kurstillfälle.

Lärandemål

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.

Kursens huvudsakliga innehåll

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.

Behörighet

Litteratur

Examination

  • EXA1 - Examination, 4,0, betygsskala: P, F

Krav för slutbetyg

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.

Ges av

EECS/Teoretisk datalogi

Kontaktperson

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

Examinator

Mads Dam <mfd@kth.se>

Versionsinformation

Kursplan gäller från och med HT2009.
Examinationsinformation gäller från och med VT2019.