 having a non-empty domain \(\mathbf{W}\) of states or worlds, a binary accessibility relation \(\mathbf{R}\) defined over it, and a collection of subsets of \(\mathbf{W}\) for each atomic proposition symbol \(P\). A modal formula \(\varphi\) is true at world \(w\) in model \(\mathcal{A}\) (\(\varphi\) is satisfied in \(\mathcal{A}\) at world \(w\)) when the following inductive conditions apply: