Action Model Logic

Origin. Baltag, Moss, Solecki (1998). General epistemic actions. Product update. Beyond announcements. Foundation of BMS framework.

Models. Action models represent epistemic actions. Product update combines model and action. Private, semi-private actions. General DEL framework.

Formalism.

Action model: A = (E, ~ᵢ, pre). E: events (action possibilities). ~ᵢ: indistinguishability for agent i. pre: preconditions (pre(e) = formula).

Example action (private announcement to i): E = {e, f}. e: actual announcement of p. f: nothing happens. ~ⱼ = E×E for j ≠ i. ~ᵢ = {(e,e), (f,f)}. pre(e) = p, pre(f) = ⊤.

Product update: M ⊗ A = (W', ~'ᵢ, V'). W' = {(w,e) : M, w ⊨ pre(e)}. (w,e) ~'ᵢ (v,f) iff w ~ᵢ v and e ~ᵢ f. Combines uncertainty.

Update operator: [A, e]ψ: after action A with actual event e, ψ. Semantics via product update. M, w ⊨ [A,e]ψ iff (w,e) ∈ W' implies M⊗A, (w,e) ⊨ ψ.

Expressivity: Strictly more expressive than PAL. Private announcements. Lies, suspicions. General communication.

Axiomatization: Reduction to epistemic logic. Complex but complete. Action model eliminated. Decidable.

Common knowledge update: Requires fixed point. Complex reduction. Group actions.

Symbols.

Symbol	Unicode	Meaning
A	—	action model
⊗	U+2297	product update
pre	—	precondition
[A,e]	—	update operator

Metatheory. Product update. General actions. Expressivity. Reduction.

Applies to. Multi-agent systems. Security protocols. Game theory. Communication.

Limitations. Complexity. Finite actions. Idealization. Protocol synthesis.