Spring 2006 (Periods III and IV)

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

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

• This course replaces the former course T-79.146 Logic in Computer Science: Special Topics I.
• Lectures: by Prof. (pro tem), D.Sc.(Tech.) Tomi Janhunen, Tuesdays 10-12, room TB353, starting on the 17th of January, 2006
• Tutorials: by M.Sc.(Tech.) Matti Järvisalo, Fridays 12-13, 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]
• In order to pass the course one has to
  • pass compulsory home assignments and
  • pass an exam (with a grade greater than 0).
• Brochure in Finnish
• Program for lectures
• Office hours: please see the lecturer's home page
• Email contacts: the alias t795101 at tcs.hut.fi is recommended.
• Newsgroup: opinnot.tik.logiikka

Lecture Notes

Refresher (.pdf)

A refresher on propositional and predicate logic

Introduction (.pdf)

Introduction to the course

Modal Logic I (.pdf)

Introduction to modal logics

Modal Logic II (.pdf)

Propositional modal logics

Modal Logic III (.pdf)

Basic results about models

Modal Logic IV (.pdf)

Some examples of modal logics

Modal Logic V (.pdf)

Hilbert-style proof theory

Modal Logic VI (.pdf)

Tableaux method

Modal Logic VII (.pdf)

More about modal logic

Modal Logic VIII (.pdf)

Introduction to temporal logics

Modal Logic IX (.pdf)

Expressing properties with temporal logic

Modal Logic X (.pdf)

Model checking

Modal Logic XI (.pdf)

Tableau method for temporal logics

Tutorials and their Solutions

• All tutorial exercises in one package: [ps] [pdf]

• 20.1. Refresher in propositional and predicate logic, solutions: [ps] [pdf]
• 27.1. Tutorial 1, solutions: [ps] [pdf]
• 3.2. Tutorial 2, solutions: [ps] [pdf]
• 10.2. Tutorial 3, solutions: [ps] [pdf]
• 17.2. Tutorial 4, solutions: [ps] [pdf]
• 3.3. Tutorial 5, solutions: [ps] [pdf]
• 17.3. Tutorial 6, solutions: [ps] [pdf]
• 24.3. Tutorial 7, solutions: [ps] [pdf]
• 31.3. Tutorial 8, solutions: [ps] [pdf]
• 7.4. Tutorial 9, solutions: [ps] [pdf]
• 21.4. Tutorial 10, solutions: [ps] [pdf]
• 28.4. Tutorial 11, solutions: [ps] [pdf]
• 5.5. Tutorial 12, solutions: [ps] [pdf]

Home Assignments

• Results of home assignments (HAs) 1-3 as of June 13, 2006.
• 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.
• Tentative schedule for spring 2006 (to be completed):

  HA	Launch date	Deadline
  1	Feb 10, 2006	Feb 28, 2006, 24:00
  2	Mar 14, 2006	Apr 4, 2006, 24:00
  3	Apr 12, 2006	May 2, 2006, 24:00

• 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. We have been reported that the version 2.5 for Windows/NT does not tolerate inputs involving inequality (!=).

Course Feedback

We welcome feedback which is collected centrally in Finnish, Swedish, or English until May 23, 2006, 24:00.

Examinations

• Exam May 18, 2006 (in Finnish, [ps] [pdf]),
  final results (published June 13, 2006)
• August 29, 2006, no examinees showed up.
• January 3, 2007, 9-12, T1
• Questions will be provided in Finnish only (unless agreed otherwise).