TCS / Studies / T-79.146 Logic in Computer Science: Special Topics I
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

[ This course has been replaced by T-79.5101 Advanced Course in Computational Logic starting from the academic year 2005-2006. ]

T-79.146 Logic in Computer Science: Special Topics I (2 cr)

Spring 2005

[General Information] [Lectures] [Tutorials] [Home assignments] [Other Interesting Stuff] [TOPI]

Previous years: [Spring 2004] [Spring 2003] [Spring 2002] [Spring 2001] [Spring 2000] [Spring 1999] [Spring 1998]

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

General Information

  • NEWS: Remember to give feedback about the course by filling out palautelomake (in Finnish) / a feedback form (in English).
    The feedback page opens on 2.5.2005 and closes on 20.5.2005.
  • Lectures by Prof. Ilkka Niemelä: Wednesday 10-12, room TB353
  • Tutorials by M.A. Misa Keinänen: Fridays 12-13, room T5
  • The course starts on Wed Jan 19 at 10.15
  • Course material:
    Lecture notes.
    M. Fitting, Basic Modal Logic, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1, Logical Foundations, 1993.
    E. Clarke and O. Grumberg and D. Peled, Model Checking, The MIT Press, 1999. (Chapters 1-4)
    E.A. Emerson, Automated Temporal Reasoning about Reactive Systems, Logics for Concurrency, F. Moller and G. Birtwistle (Eds.), Springer-Verlag, 1996, LNCS 1043, pp. 41-99.
  • In order to pass the course one has to
    • pass the home assignments
    • pass the exam (with a grade greater than 0)
  • Newsgroup: opinnot.tik.logiikka
  • Brochure in Finnish
  • Program of the course
  • Instructions for the exam.
  • Exams for the Spring 2005 course:
    10.5.2005, 13-16, T1 (paper in Finnish [PS]; results [PDF] )
    29.8.2005, 9-12, T1
    10.1.2006, 9-12, T1
Back to menu.

Lecture Notes

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

Tutorial exercises and solutions

(in Finnish) Back to menu.

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 9.2.2005 at the lecture at 10 o'clock.
    The deadline for the first assignment is Wednesday 2.3.2005.

  2. The second home assignment is distributed starting on Wednesday 16.3.2005 at the lecture at 10 o'clock. The deadline for the second assignment is 1.4.2005.

  3. The third home assignment can be obtained here ([ps] [pdf]) in electronic form starting on Wednesday 13.4.2005. The deadline is Friday 29.4.2005. See further instructions in order to get started in using the SMV tool needed in the third home assignment,

    The SMV tool has been installed at HUT/Computing Centre Unix/Linux workstations. See, SMV if you wish to install the software on your own PC.

    In the third assignment the task is to analyse a mutex algorithm whose SMV source code 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.

Back to menu.

Other Interesting Stuff

Formal methods
Information and links
Formal Methods in System Design, 22 (2) March 2003.
Special Issue on Industrial Practice of Formal Hardware Verification
Interesting books on modal logic, temporal logic and verification of reactive systems.
  • Brian F. Chellas. Modal Logic: An Introduction, Cambridge University Press, 1980.
  • Melvin Fitting. Proof Methods for Modal and Intuitionistic Logic, Reidel, 1983.
  • Robert Goldblatt. Logics of Time and Computation, CSLI Lecture Notes Number 7, Center for the Study of Language and Information, Stanford University.
  • Hughes, G.E. and Cresswell, M.J. A Companion to Modal Logic, Methuen and Co., 1984.
  • Hughes, G.E. and Cresswell, M.J. New Introduction to Modal Logic, Routledge, 1995.
  • Patrick Blackburn, Maarten de Rijke, Yde Venema. Modal Logic, Cambridge University Press, to appear in May 2001.
  • Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.
  • Zohar Manna and Richard Waldinger. The Deductive Foundations of Computer Programming. Addison-Wesley, 1993.
  • Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
  • B. Berard et al. Systems and Software Verification, Model-Checking Techniques and Tools. Springer, 2001.
  • Doron A. Peled: Software Reliability Methods, Springer 2001.
  • M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2000.
  • E. Allen Emerson. Temporal and Modal Logic. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics 1990, J. van Leeuwen, ed., North-Holland Pub. Co./MIT Press, Pages 995-1072.
Model checking tools
Back to menu.
[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 11 January 2006.

Valid HTML 4.0!