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

Metatheory. Satisfiability generally undecidable with perfect recall. Without perfect recall (synchronous, no memory): EXPSPACE. Bounded agents: better complexity. Model checking: PSPACE to EXPTIME depending on fragment. Common knowledge + time = subtle interactions. Axiomatizable with combined axioms.

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. High complexity with perfect recall. Asynchrony hard to model precisely. Common knowledge difficult computationally. Specifications hard to write correctly. Limited tool support compared to LTL alone. Interaction of modalities complex.