 Executable events and action models. To say that a pointed action model \((A,e)\) is executable at a pointed Kripke model \((M,w)\) means that \(M,w\models\pre(e)\). To say that an event f in an action model A is executable means that \((A,f)\) is executable. To say that an action model A is executable in a Kripke model M means there is an event f in A and a world v in M such that f is executable at \((M,v)\).