Arbitrary Action Model Logic and Action Model Synthesis

We present a method for synthesising action models that result in a given post-condition when executed on any Kripke model. Action models represent social actions that affect the knowledge or beliefs of agents in multi-agent systems. In the consideration of action model synthesis, we introduce an extension of the action model logic of Baltag, Moss and Solecki [3] with an action model quantifier, ∃φ which stands for “there is an action model that results in the post-condition φ”. We show that this quantifier is equivalent to the refinement quantifier of van Ditmarsch and French [10], and provide a sound and complete axiomatisation for the resulting logic, along with decidability and expressivity results.