Teacher
Davide Bresolin
Department of Mathematics
davide.bresolin[at]math.unipd.it
INF/01

Aim
Formal logic has had a central place in the study of artificial intelligence since its first conception in the 1950s. Why is this so? Logic has not been made formal just to make it suitable for computers and robots. Formal logic is also a tool for humans. Just as we could write, and execute, our grocery list and daily schedules in a computer program, so we could make our daily inferences by means of deduction in formal logic. Moreover, formal logic wasn’t even invented for machines, but to regiment and explicate human scientific reasoning. The course will give an introduction to temporal logic for students of the BMCS doctoral program. It will give the basics facts about temporal logic, to provide a common ground for further study. Then, it will show why temporal logics have become over the past 50 years very useful and important in computer science, and particularly for the formal specification, verification and synthesis of computerised systems of various nature .

Syllabus
- Brief history and philosophical origins of modal and temporal logic
- Reasoning about time.Tense and modality. Variety of temporal models
- The linear time temporal logic LTL
- Branching time and the logic CTL
- Modelling and formalising reactive systems with temporal logic
- Applications of temporal logic in computer science: specification, verification and synthesis. The model checking problem

Introductory reading
Peter Øhrstrøm and Per Hasle. Modern temporal logic: The philosophical background. In: Logic and the Modalities in the Twentieth Century, volume 7 of Handbook of the History of Logic, pages 447 – 498. North-Holland, 2006.
Clarke E.M. (2008) The Birth of Model Checking. In: 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg

Course material, enrollment and last minute notifications
Made available by the teacher at this Moodle address

Course requirements
None

Schedule
9 June, 15:00 - 17:00
11 June, 15:00 - 17:00
18 June, 15:00 - 17:00

Location
via Zoom. The link will be made available in Moodle.

<< Courses in 2019-2020