TCS / Teaching / Tik-79.146

Tik-79.146 Logic in Computer Science: Special Topics I

Spring 2001

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)
Introduction
Introduction to the course
Refresher
A refresher on propositional and predicate logic
Modal Logic I
Introduction to modal logics, syntax, semantics, basic properties
Modal Logic II
Example modal logics
Modal Logic III
Hilbert style proof theory
Modal Logic IV
Tableau Method
Modal Logic V
Translation to predicate logic, multi-modal logic, decidability and computational complexity
Modal Logic VI
Introduction to temporal logic; CTL and LTL
Modal Logic VII
CTL vs. LTL; Expressing properties of systems; model checking
Modal Logic VIII
Tableau method for CTL

Tutorials

This year we experiment by awarding points from tutorial exercises. Each tutorial has three assignments given roughly in the order of increasing difficulty, i.e., the first one is the easiest.

If you do exercises and bring the answers to a tutorial session, you can receive extra points (0-4) for the examination.

The first tutorial is a refresher on classical logic and after that there are 12 tutorials where points can be earned. So there are a total of 36 exercises on the course (3 each week). The examination points are awarded using the following table:
Exercise points Bonus exam points
6 1
12 2
18 3
24 4

However, it is not possible to change the grade from 0 to 1 with bonus points, so you have to get enough normal exam points to pass the course.

Tutorial exercises

Current point standings

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 Tuesday 6.2.2001 at the lecture 14-16 o'clock.
    The deadline for the first assignment is Tuesday 27.2.2001.

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

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

    The software (PROD/probe) that is needed in the third home assignment has been installed at HUT/Computing Centre 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: Jan 23, 2001 by Ilkka.Niemela@hut.fi