 Moreover, it is required that for every formula A and world t, G(A, t) implies M, t ⊨ A. A formula A is true in model M iff M, T ⊨ A, and A is valid with respect to a class of models if A is true in all models from that class. AT′ is semantically characterized by the following property of models: ∃t (R(T*, t, t*) and G(A, t)), and BT is characterized by ∀w∃s, t, u (R(w, s, t), R(w*, s, u), G(A, s), and R(T, t, u*)).