|
T-79.5101 |
Advanced Course in Computational Logic |
(4 cr) P |
Spring 2007 (Periods III and IV)
Navigation:
[General Information]
[Lecture Notes]
[Tutorials]
[Home Assignments]
[Feedback]
[Examinations]
[Other Interesting Stuff]
[TOPI]
Previous years:
[Spring 2006]
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.
General Information
- NEW: Course feedback is
collected from April 25, 2007 until May 23, 2007.
- This course replaces the former course
T-79.146
Logic in Computer Science: Special Topics I.
- Lectures: by Prof.
Ilkka Niemelä, Wednesdays
10-12, room TB353,
starting on the 17th of January, 2007
- Tutorials: by
M.Sc.(Tech.) Matti Järvisalo,
Mondays 12-13, 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.
[PS]
- Passing and grading of the course
- Brochure in Finnish
- Program for lectures
- Email contacts: the alias
t795101 at
tcs.hut.fi is recommended.
- Newsgroup:
[http]
Back to menu.
Lecture Notes
(In Finnish)
-
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]
- Propositional modal logics
- Modal Logic III
[ps]
[pdf]
- Basic results about models
- Modal Logic IV
[ps]
[pdf]
- Some examples of modal logics
- Modal Logic V
[ps]
[pdf]
- Hilbert-style proof theory
- Modal Logic VI
[ps]
[pdf]
- Tableaux method
- Modal Logic VII
[ps]
[pdf]
- More about modal logic
- Modal Logic VIII
[ps]
[pdf]
- Introduction to temporal logics
- Modal Logic IX
[ps]
[pdf]
- Expressing properties with temporal logic
- Modal Logic X
[ps]
[pdf]
- Model checking
- Modal Logic XI
[ps]
[pdf])
- Tableau method for temporal logics
Back to menu.
Tutorials and their Solutions
(in Finnish)
Exercise Sheets
- Tutorials 1-3: [ps]
[pdf],
solutions: [pdf]
- Tutorials 4-7: [ps]
[pdf],
solutions: [pdf]
- Tutorials 8-10: [ps]
[pdf]
solutions: [pdf]
- Tutorials 11-13: [ps]
[pdf]
solutions: [pdf]
Schedule
-
22.1. Tutorial 1
-
29.1. Tutorial 2
-
5.2. Tutorial 3
-
12.2. Tutorial 4
-
19.2. Tutorial 5
-
26.2. Tutorial 6
-
12.3 Tutorial 7
-
19.3 Tutorial 8
-
26.3. Tutorial 9
-
2.4. Tutorial 10
-
16.4. Tutorial 11
-
23.4. Tutorial 12
-
30.4. Tutorial 13
Back to menu.
Home Assignments
- Results of home assignments (HAs)
1-3 as of Mar 27, 2007.
- Each student receives three personal HAs during the spring term.
- Grading is done using the scale passed / not passed.
- Assignments will be delivered through personal
home directories.
- Home directories are created automatically for all registered students.
Passwords will be distributed when the first HA is launched.
- The schedule for Spring 2007:
HA |
Launch date |
Deadline |
1 |
Feb 7, 2007 |
Feb 21, 2007, 24:00 |
2 |
Feb 28, 2007 |
Mar 21, 2007, 24:00 |
3 |
Apr 4, 2007 |
Apr 25, 2007, 24:00 |
- In the third assignment, the task is to analyse a mutex algorithm whose
SMV source code can be found here.
- You may consult some brief instructions
to get started with SMV.
- SMV has been installed at
HUT/Computing Centre
Unix/Linux workstations.
- Check the
SMV site
at CMU if you wish to install the software on your own PC. We have
been reported that the version 2.5 for Windows/NT does not tolerate
inputs involving inequality (
!= ).
Back to menu.
Course Feedback
We welcome feedback which is collected centrally in
Finnish,
Swedish, or
English
from April 25, 2007 until May 23, 2007, 24:00.
To obtain one extra exam point you should fill in the feed back form by
the deadline (May 23, 2007). Please remember to supply your student ID on the
form. This is just to collect the list of students who have given
feedback (anonymity is not otherwise compromised).
Back to menu.
Examinations
- Material covered in exams
- May 16, 2007, 13-16, T2 (in Finnish
[pdf])
Results
- Aug 29, 2007, 9-12, T1
- Jan 4, 2008, 9-12, T1
- Questions will be provided in Finnish only
(unless agreed otherwise).
Back to menu.
Other Interesting Stuff
-
Formal methods
- 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. 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.
- M. Huth and M. Ryan.
Logic in Computer Science: Modelling and Reasoning about Systems,
Cambridge University Press, 2000.
- E. Allen Emerson. Temporal and Modal Logic. Handbook of Theoretical
Computer Science, Volume B: Formal Models and Sematics 1990, J. van
Leeuwen, ed., North-Holland Pub. Co./MIT Press, Pages 995-1072.
-
Model checking tools
Back to menu.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 24 August 2007.
|