Now that we have described the syntax of our language (that is, the set of well-formed formulas), we need semantics, that is, a formal model that we can use to determine whether a given formula is true or false. One approach to defining semantics is, as we suggested above, in terms of possible worlds, which we formalize in terms of (Kripke) structures. (In later chapters we consider other approaches to giving semantics to formulas.) A Kripke structure ##M## for ##n## agents over ##\Phi## is a tuple ##(S, π, \mathcal{K}_1, . . . , \mathcal{K}_n )##, where ##S## is a nonempty set of states or possible worlds, ##π## is an interpretation which associates with each state in ##S## a truth assignment to the primitive propositions in ##\Phi## (i.e., ##π(s) : \Phi → \{\bf{true}, \bf{false}\}## for each state ##s ∈ S##), and ##\mathcal{K}_i## is a binary relation on ##S##, that is, a set of pairs of elements of ##S##.