
T79.146 Logic in Computer Science: Special Topics I (2 cr)
Spring 2004
[General Information]
[Lectures]
[Tutorials]
[Home assignments]
[Other Interesting Stuff]
[TOPI]
Previous years:
[Spring 2003]
[Spring 2002]
[Spring 2001]
[Spring 2000]
[Spring 1999]
[Spring 1998]
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.
 NEWS:
Remember to give feedback about the course by filling out
palautelomake (in Finnish) /
a
feedback form (in English).
The feedback page opens on 3.5.2004 and closes on 31.5.2004.
 Lectures by
Prof. Ilkka Niemelä:
Wednesday 1416, room TB353
 Tutorials by
M.A. Misa Keinänen:
Fridays 1213, room TB353
 The course starts on Wed Jan 14 at 14.15
 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 14)
E.A. Emerson,
Automated Temporal Reasoning about Reactive Systems,
Logics for Concurrency, F. Moller and G. Birtwistle (Eds.),
SpringerVerlag, 1996, LNCS 1043, pp. 4199.
 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
 Program of the course
 Exam: 10.5.2004, 1316, T1:
paper in Finnish [PS];
results
 Next exams: 1.9.2004, 1316, T1 and 10.1.2005, 912, T1
 Instructions for the exam.
Back to menu.
Lecture Notes
(Slides in Finnish; Postscript/PDF form)

Refresher [ps] [pdf]
 A refresher on propositional and predicate logic

Introduction [ps] [pdf]
 Introduction to the course

Modal Logic I [ps] [pdf]
 Introduction to modal logics

Modal Logic II [ps] [pdf]
 Modal logics: syntax, semantics

Modal Logic III [ps] [pdf]
 Basic properties

Modal Logic IV [ps] [pdf]
 Example modal logics

Modal Logic V [ps] [pdf]
 Hilbert style proof theory

Modal Logic VI [ps] [pdf]
 Tableau Method

Modal Logic VII [ps] [pdf]
 Translation to predicate logic, multimodal logic, decidability and
computational complexity

Modal Logic VIII [ps] [pdf]
 Introduction to temporal logic; CTL and LTL

Modal Logic IX [ps] [pdf]
 CTL vs. LTL; Expressing properties of systems

Modal Logic X [ps] [pdf]
 Model checking CTL and LTL

Modal Logic XI [ps] [pdf]
 Tableau method for CTL
Back to menu.
Tutorial exercises and solutions
(in Finnish)
Back to menu.
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 Wednesday
28.1.2004 at the lecture 1416 o'clock.
The deadline for the first assignment is Wednesday 11.2.2004.
 The second home assignment is distributed starting on
Wednesday 3.3.2004 at the lecture 1416 o'clock.
The deadline for the second assignment is 17.3.2004.
 The third home assignment can be obtained here
([ps] [pdf]) in electronic form
starting on Wednesday
31.3.2004. The deadline is Friday 23.4.2004.
See further instructions
in order to get started in using the SMV tool needed in the third home
assignment,
The SMV tool
has been installed at
HUT/Computing Centre
Unix/Linux workstations.
See, SMV
if you wish to install the software on your own PC.
In the third assignment the task is to analyse a mutex algorithm whose
SMV source code 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.
Back to menu.
Other Interesting Stuff

Formal methods

Information and links

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. SpringerVerlag, 1992.
 Zohar Manna and Richard Waldinger. The Deductive Foundations of
Computer Programming. AddisonWesley, 1993.
 Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. SpringerVerlag, 1995.
 B. Berard et al., Systems and Software Verification, ModelChecking
Techniques and Tools. Springer, 2001.
 Doron A. Peled: Software Reliability Methods, Springer 2001.

Model checking tools

Back to menu.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 19 May 2005.
