Abstract
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 Bal tag, Moss and Solecki 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, and provide a sound and complete axiomatisation for the resulting logic, along with decidability and expressivity results.