T-79.146 Logic in Computer Science: Special Topics I
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
[Other Interesting Stuff]
- Lectures by
Prof. Ilkka Niemelš:
Wednesday 14-16, room TB353
- Tutorials by
Fridays 10-11, room TB353
- Course material:
M. Fitting, Basic Modal Logic, Handbook of Logic in
Artificial Intelligence and Logic Programming, Volume 1, Logical
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],
- Next exams: 2.9.2002, 9-12, T1; 19.12.2002, 9-12, T1
Instructions for the exam.
- Previous years:
(Slides in Finnish; Postscript form)
- A refresher on propositional and predicate logic
- 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
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
(in Finnish, Postscript format)
Paper copies of tutorials are available in the rack outside room
There are 3 compulsory home assignments
student is given a personal assignment.
The assignments can be returned at the lectures or tutorials or to the
box by the room TB336.
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.
- 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.
- The third home assignment can be obtained as a PostScript file
starting on Wednesday
10.4.2002. The deadline is Monday 29.4.2002.
For more detailed instructions, see
how to get
used by the model checker and
information on PROD
The software (PROD/probe) that is needed in the third home assignment
has been installed at HUT/Computing Centre
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
Other Interesting Stuff
Information and links
Interesting books on modal logic, temporal logic and verification of
Brian F. Chellas. Modal Logic: An Introduction,
Cambridge University Press, 1980.
- Melvin Fitting. Proof Methods for Modal and Intuitionistic Logic,
- Robert Goldblatt. Logics of Time and Computation, CSLI Lecture
Notes Number 7, Center for the Study of Language and Information,
- Hughes, G.E. and Cresswell, M.J.
A Companion to Modal Logic, Methuen and Co.,
- Hughes, G.E. and Cresswell, M.J. New Introduction to Modal Logic,
- 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.
Latest update: Dec 29, 2001