 Product update (Baltag, Moss, and Solecki 1998, 1999; see also Baltag and Moss 2004). Let \((M,w)\) be a pointed Kripke model and \((A,e)\) be a pointed action model. Let \(\models\) be a binary satisfaction relation defined between \((M,w)\) and formulas in the language \(\Lang\) of the precondition function \(\pre^A:E^A\to\Lang\) of the action model A. If \(M,w\models\pre^A(e)\), then the Kripke model   \[ M[A]=(W[A],R[A],V[A]) \]   is defined via the product update operation \(M\mapsto M[A]\) given as follows: