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	Name	Meaning
A	—	Action model	Events, indistinguishability, preconditions
⊗	U+2297	Product update	M ⊗ A: restricted product of model and action
pre	—	Precondition	Formula an event requires to occur
[A,e]	—	Update operator	After A with actual event e
E	—	Event set	Action possibilities
~ᵢ	—	Indistinguishability	Agent i cannot tell two events apart
⊤	U+22A4	Verum	Precondition of the vacuous event
⊨	U+22A8	Satisfaction	Truth at a world in a model

Metatheory. Baltag, Moss and Solecki's reduction axioms push [A, e] inward through the connectives and the knowledge operators, so every formula of action model logic without common knowledge is provably equivalent to one of multi-agent S5; completeness and decidability follow by translation, but the translation is exponential and so does not by itself transfer the PSPACE bound. With common knowledge the reduction fails — [A, e]C_Gφ has no static equivalent — and the logic is strictly more expressive than S5ₙ with C; van Benthem, van Eijck and Kooi (2006) restore a reduction by adding relativized common knowledge, and their language also admits postconditions for factual change, which the original framework lacks. Product update respects bisimulation: bisimilar models updated with bisimilar action models yield bisimilar results, which is what makes the semantics well defined on equivalence classes rather than on representations. Model checking action model logic is PSPACE-complete (Aucher and Schwarzentruber, 2013), against polynomial time for public announcement alone.

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

Limitations. Every event needs a precondition written in the object language, so an action can be modelled only to the extent that its triggering condition is already expressible; action models are finite, so unbounded or continuous protocols fall outside the framework. The original BMS system has no postconditions, so events change what is known but never what is the case, and factual change requires the substitution-augmented version. Perfect recall and logical omniscience are built into the S5 base and into product update, which never merges worlds an agent had distinguished. Adding common knowledge breaks the reduction axioms; quantifying over updates, as in arbitrary public announcement logic, makes satisfiability undecidable (French and van Ditmarsch, 2008); and multi-agent epistemic planning with action models is undecidable (Bolander and Andersen, 2011). Which action model represents a given real event is not settled by the theory.