  A frame is a structure \(\langle \bG, \bR\rangle\), where \(\bG\) is a non-empty set and \(\bR\) is a binary relation on \(\bG\). Members of \(\bG\) are states (or possible worlds). \(\bR\) is an accessibility relation. For \(\Gamma , \Delta \in \bG, \Gamma \bR \Delta\) is read “\(\Delta\) is accessible from \(\Gamma\).” A (propositional) valuation on a frame is a mapping, \(\bV\), that assigns to each propositional letter a mapping from states of the frame to truth values, true or false. For simplicity, we will abbreviate \(\bV(P)(\Gamma )\) by \(\bV(P, \Gamma )\). A propositional model is a structure  \(\cM = \langle \bG, \bR, \bV\rangle\), where \(\langle \bG, \bR\rangle\) is a frame and \(\bV\) is a propositional valuation on that frame.