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.

• Lectures by Prof. Ilkka Niemelä: Wednesday 14-16, room TB353
• Tutorials by Heikki Tauriainen: Fridays 10-11, 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.
  
• 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
• Exam: 8.5.2002, 13-16, T1, paper in Finnish [PS], paper in English [PS], results.
• Next exams: 2.9.2002, 9-12, T1; 19.12.2002, 9-12, T1
• Instructions for the exam.
• Previous years: [Spring 1998] [Spring 1999] [Spring 2000] [Spring 2001]

Lecture Notes

Refresher

A refresher on propositional and predicate logic

Introduction

Introduction to the course

Modal Logic I

Introduction to modal logics

Modal Logic II

Modal logics: syntax, semantics

Modal Logic III

Basic properties

Modal Logic IV

Example modal logics

Modal Logic V

Hilbert style proof theory

Modal Logic VI

Tableau Method

Modal Logic VII

Translation to predicate logic, multi-modal logic, decidability and computational complexity

Modal Logic VIII

Introduction to temporal logic; CTL and LTL

Modal Logic IX

CTL vs. LTL; Expressing properties of systems

Modal Logic X

Model checking CTL and LTL

Modal Logic XI

Tableau method for CTL

Tutorial exercises and solutions

• Tutorial 1 (solutions)
• Tutorial 2 (solutions)
• Tutorial 3 (solutions)
• Tutorial 4 (solutions)
• Tutorial 5 (solutions)
• Tutorial 6 (solutions)
• Tutorial 7 (solutions)
• Tutorial 8 (solutions)
• Tutorial 9 (solutions)
• Tutorial 10 (solutions)
• Tutorial 11 (solutions)
• Tutorial 12 (solutions)
• Tutorial 13 (solutions)

Home Assignments

1. The first home assignment is distributed starting on Wednesday 6.2.2002 at the lecture 14-16 o'clock.
   The deadline for the first assignment is Wednesday 27.2.2002.

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

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

   The software (PROD/probe) that is needed in the third home assignment has been installed at HUT/Computing Centre Alpha 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.

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.

• 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.