TCS /
Teaching /
Tik-79.146
Tik-79.146 Logic in Computer Science: Special Topics I
Spring 2001
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]
[Tutorials]
[Home assignments]
[Program]
[Other Interesting Stuff]
- Lectures by
Prof. Ilkka Niemelä:
Tuesdays 14-16, room T4
- Tutorials by
Heikki Tauriainen:
Fridays 12-13, room TB353
- Course material:
Lecture notes.
Fitting, Basic Modal Logic, Handbook of Logic in
Artificial Intelligence and Logic Programming, Volume 1, Logical
Foundations, 1993.
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
,
course information at
TOPI
- Exam: 8.5.2001, 13-16, T1, paper [PS],
results.
- Next exams: 10.9.2001, 13-16, T1; 14.12.2001, 13-16, T1
-
Instructions for the exam.
- Previous years:
[Spring 1998]
[Spring 1999]
[Spring 2000]
Lecture Notes
(Slides in Finnish; Postscript form)
-
Introduction
- Introduction to the course
-
Refresher
- A refresher on propositional and predicate logic
-
Modal Logic I
- Introduction to modal logics, syntax, semantics, basic properties
-
Modal Logic II
- Example modal logics
-
Modal Logic III
- Hilbert style proof theory
-
Modal Logic IV
- Tableau Method
-
Modal Logic V
- Translation to predicate logic, multi-modal logic, decidability and
computational complexity
-
Modal Logic VI
- Introduction to temporal logic; CTL and LTL
-
Modal Logic VII
- CTL vs. LTL; Expressing properties of systems; model checking
-
Modal Logic VIII
- Tableau method for CTL
Tutorials
This year we experiment by awarding points from tutorial
exercises. Each tutorial has three assignments
given roughly in the order of increasing difficulty, i.e., the first one
is the easiest.
If you do exercises and bring the answers to a tutorial
session, you can receive extra points (0-4) for the examination.
The first tutorial is a refresher on classical logic and after that
there are 12 tutorials where points can be earned.
So there are a total of 36 exercises on the course (3 each week).
The examination points are awarded using the following table:
Exercise points | Bonus exam points |
6 | 1 |
12 | 2 |
18 | 3 |
24 | 4 |
However, it is not possible to change the grade from 0 to 1 with bonus
points, so you have to get enough normal exam points to pass the course.
Tutorial exercises
Current point standings
Home Assignments
There are 3 compulsory home assignments
(see Program).
Each
student is given a personal assignment.
-
The first home assignment is distributed starting on Tuesday 6.2.2001 at the
lecture 14-16 o'clock.
The deadline for the first assignment is Tuesday 27.2.2001.
- The second home assignment is distributed starting on
Tuesday 13.3.2001 at the lecture 14-16 o'clock.
The deadline for the second assignment is Tuesday 3.4.2001.
- The third home assignment can be obtained as a PostScript file
here
starting on Tuesday
10.4.2001. The deadline is Wednesday 2.5.2001.
For more detailed instructions, see
how to get
started,
general
information and
CTL syntax
used by the model checker.
The software (PROD/probe) that is needed in the third home assignment
has been installed at HUT/Computing Centre
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.
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
-
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.
- E. Clarke and O. Grumberg and D. Peled.
Model Checking, The MIT Press, 1999.
- 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.
Latest update: Jan 23, 2001
by Ilkka.Niemela@hut.fi