Temporal Logics and Tableaux
Lecturer: Valentin Goranko
Location: Room 3513, Teaching Building No.3, Tsinghua University
Time: Wednesday 9:50-12:15, from March 20th to May 8th, 2024.
==Course Description==
This course will introduce and discuss some of the most important types and systems of temporal logics, including instant-based logics of linear and branching time, as well as some temporal logics for multi- agent systems. The course will also present tableaux-based decision methods for some of these logics. Time permitting, it may also cover a selection of additional topics, such as interval-based temporal logics, temporal-epistemic logics, or first-order temporal logics.
The course is intended as interdisciplinary, for a broad audience of mainly graduate students interested in logical, philosophical, and computational aspects of temporal reasoning.
==Outline of Main Topics and Tentative Schedule==
The course will comprise six 135-minute long lecture sessions, tentatively planned as follows:
Lecture session 1.
- Introduction. Reasoning about time: brief history and philosophical origins. Time, tense, and modality. Models and properties of time flows.
- Prior’s basic temporal logic and some extensions of it.
Temporal logics over linear time flows. Additional temporal operators: Nexttime, Since, and Until. The linear time temporal logic LTL (briefly).
Lecture session 2.
- Diodorus’ Master Argument and related arguments formalised.
Branching time temporal logics as possible solutions. Models of branching time and historical necessity. - Peircean branching time temporal logics. Ockhamist branching time temporal logics. Branching time temporal logics in computer science: CTL and CTL* (briefly).
Lecture session 3.
- Tableaux-based methods for modal and temporal logics:
– preliminaries on tableaux for classical propositional logic.
– a general framework for the incremental tableaux method: main components and closures of formulae, full expansions, pre-tableaux construction phase and initial tableaux, elimination phase and final tableaux. Open and closed tableaux and constructing models from open tableaux.
Lecture session 4.
- Incremental tableaux-based decision procedures for the temporal logics LTL and CTL.
Lecture session 5.
- Alternating time temporal logic ATL and some variations and extensions. Outline of tableaux for ATL.
Lecture session 6.
- The temporal logic of coalitional goal assignments TLCGA and some variations.
Alternative optional topics.
1. Interval-based temporal logics on linear time flows. 2. Temporal epistemic logics.
3. First-order temporal logics.
==Expected Level and Pre-requisites==
The course is intended for a broad audience with basic knowledge of classical and modal logics. The intended level is middle graduate, but it can be adjusted up or down, depending on the actual audience.
==Selected references==
- Valentin Goranko. Temporal Logics, Cambridge University Press, 2023.
- Valentin Goranko and Antje Rumberg. Temporal Logic, Stanford Encyclopedia of Philosophy, 2024.
- John Burgess. Basic tense logic, in Gabbay and Guenthner (eds.), Handbook of Philosophical Logic, 2nd edition, Volume 7, Gabbay and Guenthner (eds.) (2002), pp. 142.
- St ́ephane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science. CUP, 2016.
- Rob Goldblatt. Logics of Time and Computations. CSLI pubblications, 2nd revised and expanded edition, 1992.
- P. Øhrstrøm and Per Hasle. Temporal Logic: From Ancient Ideas to Artificial Intelligence. Kluwer, 1995. (Reprinted by Springer).
- A.N. Prior. Past, Present and Future. Oxford University Press, 1967.
- Yde Venema. Temporal Logic, chapter in: Lou Goble (ed), Blackwell Guide on Philosophical Logic,Blackwell Publishers, 2001, pp 203-211
Relevant parts of these plus additional readings will be made available to the participants in the course.