TCS / Studies / T-79.5101 Advanced Course in Computational Logic
Helsinki University of Technology, Laboratory for Theoretical Computer Science

T-79.5101

Advanced Course in Computational Logic

(4 cr) P

Spring 2008 (Periods III and IV)

Navigation: [General Information] [Lecture Notes] [Tutorials] [Home Assignments] [Feedback] [Examinations] [Other Interesting Stuff] [TOPI]

Previous years: [Spring 2006] [Spring 2007]

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

  • NEW: Course feedback is collected from April 28, 2008 until May 20, 2008.
  • This course replaces the former course T-79.146 Logic in Computer Science: Special Topics I.
  • Lectures: by Prof. Ilkka Niemelä, Tuesdays 10-12, room TB353, starting on Jan 22, 2008
  • Tutorials: by Lic.Sc.(Tech.) Matti Järvisalo, Mondays 15-16, room TB353
  • 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. [PS]
  • Passing and grading of the course
  • In order to pass the course one has to
    • pass compulsory home assignments and
    • pass the final exam (with a grade greater than 0).
  • Brochure in Finnish
  • Program for lectures + slides
  • Email contacts: the alias t795101 at tcs.hut.fi is recommended.
  • Newsgroup: [http]
Back to menu.

Tutorials and their Solutions

Exercise Sheets

  • Exercises 1-3: [ps] [pdf], solutions: [ps] [pdf]
  • Exercises 4-7: [ps] [pdf], solutions: [ps] [pdf]
  • Exercises 8-10: [ps] [pdf], solutions: [ps] [pdf]
  • Exercises 11-13: [ps] [pdf], solutions: [ps] [pdf]

Participation

Home Assignments

  • Results of home assignments (HAs) 1-3
  • Each student receives three personal HAs during the spring term.
  • Grading is done using the scale passed / not passed.
  • Assignments will be delivered through personal home directories.
  • Home directories are created automatically for all registered students. Passwords will be distributed when the first HA is launched.
  • The schedule for Spring 2008:

    HA Launch date Deadline
    1 Feb 12, 2008 Feb 26, 2008, 23:59
    2 Mar 4, 2008 Mar 26, 2008, 23:59
    3 Apr 8, 2008 Apr 29, 2008, 23:59

  • In the third assignment, the task is to analyse a mutex algorithm whose SMV source code can be found here.
  • You may consult some brief instructions to get started with SMV.
  • SMV has been installed at HUT/Computing Centre Unix/Linux workstations.
  • Check the SMV site at CMU if you wish to install the software on your own PC.
Back to menu.

Course Feedback

We welcome feedback which is collected centrally in Finnish, Swedish, or English from April 28, 2008 until May 20, 2008, 23:58.

To obtain one extra exam point you should fill in the feed back form by the deadline (May 20, 2008). Please remember to supply your student ID on the form. This is just to collect the list of students who have given feedback (anonymity is not otherwise compromised).

Back to menu.

Examinations

Back to menu.

Other Interesting Stuff

  • Formal methods
  • 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: 09 May 2008.