TCS / Teaching / Tik-79.146

Tik-79.146 Logic in Computer Science: Special Topics I

Spring 2000

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] [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
tutorial 1 (solutions)
Modal Logic I
Introduction to modal logics, syntax, semantics, basic properties
tutorial 2 (solutions)
tutorial 3 (solutions)
tutorial 4 (solutions)
Modal Logic II
Example modal logics
tutorial 5 (solutions)
Modal Logic III
Hilbert style proof theory
tutorial 6 (solutions)
Modal Logic IV
Tableau Method
tutorial 7 (solutions)
tutorial 8 (solutions)
Modal Logic V
Translation to predicate logic, multi-modal logic, decidability and computational complexity
tutorial 9 (solutions)
Modal Logic VI
Introduction to temporal logic; CTL and LTL
tutorial 10 (solutions)
Modal Logic VII
CTL vs. LTL; Expressing properties of systems; model checking
tutorial 11 (solutions)
tutorial 12 (solutions)
Modal Logic VIII
Tableau method for CTL
tutorial 13 (solutions)

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 Thursday 10.2.2000 at the lecture 16-18 o'clock.
    The deadline for the first assignment is Thursday 2.3.2000.

  2. The second home assignment is distributed starting on Thursday 23.3.2000 at the lecture 16-18 o'clock. The deadline for the second assignment is Thursday 6.4.2000.

  3. The third home assignment can be obtained as a PostScript file here starting on Thursday 6.4.2000. The deadline is Friday 5.5.2000. For more detailed instructions, see how to get started, general information and CTL syntax used by the model checker.
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


Latest update: Feb 2, 2000 by Ilkka.Niemela@hut.fi