Lecture 1

• Introduction
• Historical development of modal and temporal logic
• Classification of approaches: flows of time; linear vs branching; modal vs. first-order; point based vs interval based, etc.
• Minimal modal logic, K, Kripke semantics
• Prior's Tense Logic, TL

Lecture 2

• Hilbert-style systems for modal and tense logics
• Frame definability
• Completeness via canonical model construction
• Completeness via the mosaic method
• Complexity of satisfiability and model checking for K and for TL

Lecture 3

• First-order logic, standard translation of modal and tense logic into FO
• Ehrenfeucht-Fraisse games
• compositionality on linear time frames
• collapse of FO to its 3-variable fragment FO³ on linear orders
• separation property of FO, "separation = composition + relativisation"
• failure of separation for FO², the temporal operator "Until" U

Lecture 4

• Gabbay's separation theorems
• Kamp's theorem, proof via "short games" and "decomposition formulas"
• Incompleteness in the presence of gaps, Stavi's operators
• Satisfiability over the reals and various natural classes of time frames

Lecture 5

• LTL on finite words, Wilke's construction from counter-free DFA to equivalent LTL fromula
• LTL model checking and satisfiability via Büchi automata, PSPACE-completeness
• characterisation of the fragments TL[X], TL[F], towards TL[X,F]

Lecture 6

• Primer on ω-regular languages, Büchi automata, ω-regular expressions, normal forms
• McNaughton's theorem and consequences
• Landweber hierarchy, classification of LTL specifications
• adding past modality: LTL+P, normal form, succinctness
• non-existence of finite basis for ω-regular events
• non-existence of finite basis for the future fragment of FO on ordinals, reals

Lecture 7

• Branching time logics primer: Ockhamist vs. Peircean semantics
• The linear time vs. branching time debate (cf. Lamport, Emerson-Halpern)
• Computation Tree Logic, CTL and some extensions: ECTL, ECTL⁺, CTL^*,
  first-order path modalities and the logics BTL_m
• FO on trees: weakness, Schlingloff's characterisation (without proof)
• monadic second-order logic, monadic path logic, MPL, composition theorems for trees
• ECTL⁺ ≡ BTL₂; CTL^* ≡ ∪_mBTL_m
• CTL^* captures the bisimulation invariant fragment of (future) MPL

Lecture 8

• counting CTL* with "Since" captures monadic path logic
• Weak Alternating Automata on trees: closure properties, relation to Büchi automata,
  natural devices for CTL and extensions (for LTL on words)


• Interval temporal logics primer
• Example: causaily in Minkowsky spacetime; non-example: Future Interval Logic
• Allen's relations and Halpern-Shoham Logic: frame definability, interdefinability of operators.
• Venema's CDT logic

Lecture 9

• Expressiveness of Venema's logic: CDT ≡ FO³
• Propositional Neighborhood Logic PNL = HS[A,A^-1,π],
  its expressive completeness: PNL ≡ FO², and decidability of FO² (without proof)
• Undecidability results via encoding Turing machine computations and tilings
• Undecidability of HS[D] on finite interval structures.
• Decidability of HS[A,B,B^-1] on the naturals, and of HS[A,A^-1,B,B^-1] on finite interval structures (proof sketch).

Lecture 10

• Recap of basic notions of interval temporal logics
• Rudiments of Timed Automata, semantics based on timed words
• Region automaton construction, decidability of emptiness
• Undecidability of universality, no complementation, no determinisation
• Possible extensions of timed automata
• Some special cases with decidable language inclusion

Lecture 11

• Timed extensions of branching time and linear time logics
• Comparison of continuous versus point-wise semantics
• Timed variants of temporal modalities versus hybrid extensions with clock variables and the freeze quantifier
• high undecidability of satisfiability
• decidability and complexity of model checking TCTL and (only in the point-wise semantics) MTL

Lecture 12

• Decidable cases/fragments of MTL satisfiability and model checking in pointwise semantics:
  • decidability of MTL on finite timed words via translation into 1-clock alternating timed automata
  • decidability of SafetyMTL on infinite timed words via 1-clock alternating TA
  • non-primitive recursive complexity of 1-clock alternating TA via lossy channel machines
• Decidable cases/fragments of MTL in continuous semantics:
  • on bounded intervals: EXPSPACE-completeness of MTL,
    decidability of FO[<,+1] and of MSO[<,+1] (for finite variability signals only)
  • EXPSPACE-completeness of Metric Interval Temporal Logic MITL

Intros and historical surveys

Robert Goldblatt, Mathematical Modal Logic: A view of its evolution,
Journal of Applied Logic 1 (5-6), pp. 309 - 392, 2003.

Peter Øhrstrøm, Per F. V. Hasle, A.N. Prior's Rediscovery of Tense Logic,

E. Allen Emerson, Temporal and Modal Logic,
in the Handbook of Theoretical Computer Science, J. van Leeuwen, ed., North Holland, 1995.

Yde Venema, Temporal Logic,
in: L Goble (ed.), The Blackwell Guide to Philosophical Logic, Blackwell Publishers, 2001.

Sara L. Uckelman, Lecture Notes: Temporal Logic,
Lecture Notes, Univ. Amsterdam, 2010.

Peter Øhrstrøm, Per F. V. Hasle, Temporal logic: from ancient ideas to artificial intelligence,
on פooƃlǝ books

Moshe Y. Vardi, From Church and Prior to PSL,
in 25 Years of Model Checking: History, Achievements, Perspectives, LNCS 5000, 2008.

Edmund M. Clark, The Birth of Model Checking,
in 25 Years of Model Checking: History, Achievements, Perspectives, LNCS 5000, 2008.

E. Allen Emerson, The Beginning of Model Checking: A Personal Perspective,
in 25 Years of Model Checking: History, Achievements, Perspectives, LNCS 5000, 2008.

General References

Edmund M. Clarke, Bernd-Holger Schlingloff, Model Checking,
in Handbook of Automated Reasoning, 2000.

Axiomatic completeness, Complexity of satisfiability and model checking

Yde Venema, Temporal Logic,
in: L Goble (ed.), The Blackwell Guide to Philosophical Logic, Blackwell Publishers, 2001.

Maarten Marx, Szabolcs Mikulás, Mark Reynolds The Mosaic Method for Temporal Logics,
in Automated Reasoning with Analytic Tableaux and Related Methods, LNCS 1847, pp. 324-340, 2000.

Philippe Schnoebelen, The Complexity of Temporal Logic Model Checking,
Advances in Modal Logic 4, 2003.

Expressive completeness, Kamp's theorem, Gabbay's separation

Edmund M. Clarke, Bernd-Holger Schlingloff, Model Checking,
in Handbook of Automated Reasoning, 2000.

Ian Hodkinson, Notes on games in temporal logic,
Lecture notes for LUATCS meting, Johannesburg, Dec 1999.

Dov Gabbay, Ian Hodkinson, Mark Reynolds, Temporal Expressive Completeness in the Presence of Gaps,
ASL Logic Colloquium '90, Lecture Notes in Logic 2:89-121, 1993.

Mark Reynolds, The Complexity of Temporal Logic over the Reals,
Annals of Pure and Applied Logic, 2010.

Mark Reynolds, The complexity of the temporal logic with "until" over general linear time,
J. of Comp. Syst. Sciences 66(2) : 393-426, 2003.

John P. Burgess, Yuri Gurevich, The Decision Problem for Linear Temporal Logic,
Notre Dame Journal of Formal Logic26(2):115-128, 1985.

Dov Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi On the temporal analysis of fairness,
in 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1980.

Joëlle Cohen, Dominique Perrin, Jean-Eric Pin On the expressive power of temporal logic,
Temporal Logic, 1991.

LTL, ω-regular languages, Büchi automata, monadic second-order logic

Wolfgang Thomas, Languages, Automata, and Logic, in Handbook of Formal Languages, vol. III, pp. 389-455, 1997.

Thomas Wilke, Classifying Discrete Temporal Properties,
in Proc. STACS'99, pp. 32-46, 1999.

Thomas Wilke, Linear Temporal Logic and Finite Semigroups,
in Proc. MFCS'01, pp. 96-110, 2001.

A. Prasad Sistla, Lenore D. Zuck, Reasoning in a restricted temporal logic,
Information and Computation 102, pp. 167-195, 1993.

Nicolas Markey, Temporal Logic with Past is Exponentially more Succinct,
in EATCS Bull. 79: 122-128, 2003.
See also: Temporal Logic with Past is Exponentially More Succinct

Non-existence of finite basis

D. Beauquier, A. Rabinovich, Monadic Logic of Order over Naturals Has no Finite Base,
Journal on Logic and Computations 12:(2) pp. 243-253, 2002.

Yoram Hirshfeld Alexander Rabinovich, Future temporal logic needs infinitely many modalities,
Information and Computation 187(2): 196-208, 2003.

Branching Time Logics

E. Allen Emerson, Joseph Y. Halpern,
"Sometimes" and "Not never" Revisited: On Branching Versus Linear Time Temporal Logic,
J. of ACM, vol. 33(1), 1986.

E. Allen Emerson, Joseph Y. Halpern,
Decision Procedures and Expressiveness in the Temporal Logic of Branching Time,
J. of Comp. Syst. Sci. 30(1), 1985.

Moshe Y. Vardi, Branching vs. Linear Time: Final Showdown,
Invited talk at ETAPS 2001.

Faron Moller, Alexander Rabinovich Counting on CTL^*: On the Expressive Power of Monadic Path Logic,
Information and Computation 184(1), 2003.

Faron Moller, Alexander Rabinovich BTL₂ and the expressive power of ECTL⁺,
Information and Computation 204(7), 2006.

Bernd-Holger Schlingloff Expressive Completeness of Temporal Logic of Trees,
Journal of Applied Non-Classical Logics, vol. 2(2), 1992.

Weak Alternating Automata

David E. Muller, Ahmed Saoudi, Paul E. Schupp,
Weak Alternating Automata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time, in Proc. LICS 1988.

David E. Muller, Ahmed Saoudi, Paul E. Schupp,
Alternating automata, the weak monadic theory of the tree, and its complexity,
Automata, Languages and Programming, 1986.

Moshe Vardi, Alternating Automata: Checking Truth and Validity for Temporal Logics,
Automated Deduction -- CADE, 1997.

Christof Löding, Wolfgang Thomas, Alternating Automata and Logics over Infinite Words,
in Proc. IFIP TCS 2000.

Interval Temporal Logics

Ilya Shapirovsky, Valentin Shehtman, Chronological future modality in Minkowski spacetime,
Advances in Modal Logic, 4:437-459, 2003.

Davide Bresolin, Dario Della Monica, Valentin Goranko, Angelo Montanari, Guido Sciavicco,
Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification,
in Proc. LPAR 2010.

Davide Bresolin, Valentin Goranko, Angelo Montanari, Guido Sciavicco,
On Decidability and Expressiveness of Propositional Interval Neighborhood Logics, in Proc. LFCS 2007.

Davide Bresolin, Valentin Goranko, Angelo Montanari, Guido Sciavicco,
Propositional Interval Neighborhood Logics: Expressiveness, Decidability, and Undecidable Extensions,
Annals of Pure and Applied Logic 161(3):289-304, 2009.

The Last Paper on the Halpern-Shoham Interval Temporal Logic
Draft at arXiv:1010.4529v1 [cs.LO], 21 Oct 2010.

Angelo Montanari, Gabriele Puppis, Pietro Sala, Guido Sciavicco,
Decidability of the interval temporal logic ABB' over the natural numbers, , in Proc. STACS 2010.

Angelo Montanari, Gabriele Puppis, Pietro Sala,
Maximal decidable fragments of Halpern and Shoham's modal logic of intervals,, in Proc. ICALP 2010.

Martin Otto, Two Variable First-Order Logic over Ordered Domains,
Journal of Symbolic Logic, 66(2):685-702, 2001.

Timed automata and Timed temporal logics

Rajeev Alur, David L. Dill, A Theory of Timed Automata,
Theor. Comp. Sci., 126:183-235, 1994.

Rajeev Alur, P. Madhusudan, Decision Problems for Timed Automata: A Survey
in Proc. SFM-RT 2004, LNCS 3185.

Patricia Bouyer, Francois Laroussinie, Model checking timed automata
Chapter 4 of Modeling and Verification of Real-Time Systems, 2008.

Rajeev Alur, Thomas Henzinger, A really temporal logic,
Journalf of the ACM, 41:181-204, 1994.

Rajeev Alur, Thomas Henzinger, Real-Time Logics: Complexity and Expressiveness
Inf. and Comp., 104(1): 35-77, 1993.

R. Alur, T. Feder, Th. Henzinger, The Benefits of Relaxing Punctuality,
Journal of the ACM, 43, 1996.

Joël Ouaknine, James Worrell On the decidability of Metric Temporal Logic
in Proc. LICS 2005.

Joël Ouaknine, James Worrell Some Recent Results in Metric Temporal Logic
in Proc. FORMATS 2008.

Slawomir Lasota, Igor Walukiewicz, Alternating Timed Automata,
ACM Trans. Comp. Logic, vol. 9(2), 2008.

Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, James Worrell
Universality Analysis for One-Clock Timed Automata,
Fundamenta Informaticae, 2008.

Patricia Bouyer, Model-Checking Timed Temporal Logics,
In M4M-5, ENTCS 231, pp. 323-341, 2009.

Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James Worrell
On Expressiveness and Complexity in Real-time Model Checking,
In Proc. ICALP'08, LNCS 5126, pages 124-135. 2008.