TCS /
Teaching /
Tik79.146
Tik79.146 Logic in Computer Science: Special Topics I
Spring 2000
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]
[Home assignments]
[Program]
[Other Interesting Stuff]
 Lectures by
Docent Ilkka Niemelä:
Thursdays 1618, room T4
 Tutorials by
Heikki Tauriainen:
Fridays 1516, room T4
 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.),
SpringerVerlag, 1996, LNCS 1043, pp. 4199.
Articles.
 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
(PostScript),
course information at
TOPI
 Exam: 12.5.2000, 1316, T1

Results
of the exam on 12.5.2000

Instructions for the exam.
 Previous years:
[Spring 1998]
[Spring 1999]
Lecture Notes
(Slides in Finnish; Postscript form)

Introduction
 Introduction to the course

Refresher
 A refresher on propositional and predicate logic
tutorial 1
(solutions)

Modal Logic I
 Introduction to modal logics, syntax, semantics, basic properties
tutorial 2
(solutions)
tutorial 3
(solutions)
tutorial 4
(solutions)

Modal Logic II
 Example modal logics
tutorial 5
(solutions)

Modal Logic III
 Hilbert style proof theory
tutorial 6
(solutions)

Modal Logic IV
 Tableau Method
tutorial 7
(solutions)
tutorial 8
(solutions)

Modal Logic V
 Translation to predicate logic, multimodal logic, decidability and
computational complexity
tutorial 9
(solutions)

Modal Logic VI
 Introduction to temporal logic; CTL and LTL
tutorial 10
(solutions)

Modal Logic VII
 CTL vs. LTL; Expressing properties of systems; model checking
tutorial 11
(solutions)
tutorial 12
(solutions)

Modal Logic VIII
 Tableau method for CTL
tutorial 13
(solutions)

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 Thursday 10.2.2000 at the
lecture 1618 o'clock.
The deadline for the first assignment is Thursday 2.3.2000.
 The second home assignment is distributed starting on
Thursday 23.3.2000 at the lecture 1618 o'clock.
The deadline for the second assignment is Thursday 6.4.2000.
 The third home assignment can be obtained as a PostScript file
here
starting on Thursday
6.4.2000. The deadline is Friday 5.5.2000.
For more detailed instructions, see
how to get
started,
general
information and
CTL syntax
used by the model checker.
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
Latest update: Feb 2, 2000
by Ilkka.Niemela@hut.fi