Epistemic Temporal Logic

Origin. Combines epistemic and temporal logics (1980s-90s). Also called the temporal logic of knowledge. Halpern, van der Meyden, and Vardi developed foundations. Knowledge changes over time; time reveals information. Security protocols, distributed systems need both. Tools: MCK, MCMAS.

Models. Knowledge evolving over time. Epistemic: what agents know at a moment. Temporal: how things change over time. Combined: what agents know, knew, will know. "Alice will eventually know the secret." "Bob knew before Carol did."

Formalism.

Combined syntax: φ ::= p | ¬φ | φ ∧ ψ | Kₐφ | Cᴳφ | Xφ | φUψ | Gφ | Fφ

Epistemic: Kₐ (a knows), Cᴳ (common knowledge in G) Temporal: X (next), U (until), G (always), F (eventually)

Point: (r, m): run r at time m — the unit of evaluation.

Interpreted systems: I = (R, π) where:

R ⊆ (Lₑ × L₁ × ... × Lₙ)^ω (runs: sequences of global states)
Each agent i has local state from Lᵢ
Environment has state from Lₑ
π: global states → 2^AP

Semantics: (I, r, m) ⊨ Kₐφ iff ∀(r', m'). r(m) ~ₐ r'(m') implies (I, r', m') ⊨ φ

Where r(m) ~ₐ r'(m') means a's local state same.

Synchronous vs asynchronous: Synchronous: agents share clock (m = m' in ~ₐ). Asynchronous: no shared clock (harder to verify).

Key formulas:

Kₐ Fφ: "a knows φ will happen"
F Kₐφ: "a will know φ"
G(Kₐφ → Kᵦφ): "whenever a knows, b knows"
K_a G safe: "a knows system is always safe"

Perfect recall: Agents remember their history. ~ₐ defined on prefixes of runs.

Symbols.

Symbol	Unicode	Name	Meaning
Kₐ	—	Knows	Agent a knows
Cᴳ	—	Common	Common knowledge
X	—	Next	Next moment
G	—	Globally	Always
F	—	Finally	Eventually
U	—	Until	Until
~ₐ	—	Indistinguishable	Same local state
(r, m)	—	Point	Run r at time m: the unit of evaluation
I	—	Interpreted system	Set of runs plus a valuation
R	—	Run set	Admissible histories of the system
Lᵢ	—	Local state set	States agent i can be in
π	U+03C0	Valuation	Global states to sets of atoms
ω	U+03C9	Omega	Runs are ω-sequences of global states
⊨	U+22A8	Satisfaction	Truth at a point of a system
∀	U+2200	Universal quantifier	Over indistinguishable points
⊆	U+2286	Inclusion	R as a set of global-state sequences

Metatheory. Halpern and Vardi (1989) mapped the field by classifying logics of knowledge and time along independent parameters — perfect recall or not, synchrony or not, presence of common knowledge, unique initial state — and showed complexity turns sharply on each. Under observational semantics, where knowledge depends only on the current local state, validity for the linear-time epistemic language without common knowledge is PSPACE-complete, the same as LTL alone. Perfect recall raises it steeply, and perfect recall together with common knowledge makes validity Π¹₁-complete, so those systems are not recursively axiomatizable at all. Halpern, van der Meyden and Vardi (2004) gave complete axiomatizations for the classes that are, the characteristic interaction axiom for synchronous perfect recall being Kₐ X φ → X Kₐ φ; the converse, X Kₐ φ → Kₐ X φ, characterizes no learning. Model checking splits the same way: decidable for the observational reading, undecidable with perfect recall and common knowledge (van der Meyden and Shilov, 1999).

Applies to. Security protocol analysis (what attacker learns when). Distributed systems (consensus, agreement). Game theory (information over time). Privacy (inference from observations). Verification of multi-agent systems. Authentication protocols.

Limitations. Π¹₁-completeness of validity for perfect recall with common knowledge is a difference in kind, not in cost: no finitary proof system is complete for those systems, and van der Meyden and Shilov's result puts model checking beyond decidability as well. Knowledge is defined by indistinguishability of local states, so it is S5 — the agent is logically omniscient and fully introspective, and knows every consequence of its local state including facts it has no means of computing. Perfect recall means unbounded memory, which is why the state space becomes histories rather than states. By Halpern and Moses (1990) common knowledge is unattainable in asynchronous systems and in systems with unreliable channels, so specifications requiring it describe a limit no run reaches. Nothing in the framework fixes what the local states are, yet that choice determines every knowledge claim and is made outside the logic.