”
Time is what keeps everything from happening at
once _{— Ray Cummings}
Lecture summary
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^{3} on linear orders
- separation property of FO,
"separation = composition + relativisation"
- failure of separation for FO^{2},
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_{2};
CTL^{*} ≡ ∪_{m}BTL_{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^{3}
- Propositional Neighborhood Logic
PNL = HS[A,A^{-1},π],
its expressive completeness:
PNL ≡ FO^{2},
and decidability of FO^{2}
(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
Some reading material
Intros and historical surveys
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.
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.
Expressive completeness, Kamp's theorem, Gabbay's separation
Edmund M. Clarke, Bernd-Holger Schlingloff,
Model Checking,
in Handbook of Automated Reasoning, 2000.
LTL, ω-regular languages, Büchi automata, monadic second-order logic
Non-existence of finite basis
Branching Time Logics
Weak Alternating Automata
Interval Temporal Logics
Timed automata and Timed temporal logics
Last updated on 5 January 2011