TCS / Teaching / T-79.146

T-79.146 Logic in Computer Science: Special Topics I

Spring 2002

This is an advanced course on logic and its applications in computer science and engineering. Subjects covered this year are: modal logics (syntax, semantics, proof theory and computational properties) and applications of temporal logic in concurrent and distributed systems.

[Lecture Notes] [Tutorials] [Home assignments] [Program] [Other Interesting Stuff]

Lecture Notes

(Slides in Finnish; Postscript form)
A refresher on propositional and predicate logic
Introduction to the course
Modal Logic I
Introduction to modal logics
Modal Logic II
Modal logics: syntax, semantics
Modal Logic III
Basic properties
Modal Logic IV
Example modal logics
Modal Logic V
Hilbert style proof theory
Modal Logic VI
Tableau Method
Modal Logic VII
Translation to predicate logic, multi-modal logic, decidability and computational complexity
Modal Logic VIII
Introduction to temporal logic; CTL and LTL
Modal Logic IX
CTL vs. LTL; Expressing properties of systems
Modal Logic X
Model checking CTL and LTL
Modal Logic XI
Tableau method for CTL

Tutorial exercises and solutions

(in Finnish, Postscript format) Paper copies of tutorials are available in the rack outside room TB336.

Home Assignments

There are 3 compulsory home assignments (see Program). Each student is given a personal assignment.
  1. The first home assignment is distributed starting on Wednesday 6.2.2002 at the lecture 14-16 o'clock.
    The deadline for the first assignment is Wednesday 27.2.2002.

  2. The second home assignment is distributed starting on Wednesday 6.3.2002 at the lecture 14-16 o'clock. The deadline for the second assignment is Tuesday 27.3.2001.

  3. The third home assignment can be obtained as a PostScript file here starting on Wednesday 10.4.2002. The deadline is Monday 29.4.2002. For more detailed instructions, see how to get started, CTL syntax used by the model checker and general information on PROD

    The software (PROD/probe) that is needed in the third home assignment has been installed at HUT/Computing Centre Alpha workstations

    See, PROD if you wish to install the software on your own PC. In the third assignment the task is to analyse a mutex algorithm whose Pr/T-net model can be found here.

The assignments can be returned at the lectures or tutorials or to the box by the room TB336.

If you cannot come to pick up your assignment at the lectures, please contact the lecturer directly.

If you have returned your assignment, see the results.

Other Interesting Stuff

Formal methods
Information and links
Interesting books on modal logic, temporal logic and verification of reactive systems.

Latest update: Dec 29, 2001 by