form in Kripke structures, also known as Kripke models. A Kripke structure M for n agents over is an (n + 2)-tuple , 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 (the set of all primitive propositions), and are binary relations on S for n numbers of agents. It is important here not to confuse , our modal operator, and , our accessibility relation. The truth assignment tells us whether or not a proposition p is true or false in a certain state. So tells us whether p is true in state s in model . Truth depends not only on the structure, but on the current world as well. Just because something is true in one world does not mean it is true in another. To state that a formula is true at a certain world, one writes , normally read as " is true at (M,s)," or "(M,s) satisfies ". It is useful to think of our binary relation as a possibility relation, because it is meant to capture what worlds or states agent i considers to be possible; In other words, if and only if , and such 's are called epistemic alternatives for agent i. In idealized accounts of knowledge (e.g., describing the epistemic status of perfect reasoners with infinite memory capacity), it makes sense for to be an equivalence relation, since this is the strongest form and is the most appropriate for the greatest number of applications. An equivalence relation is a binary relation that is reflexive, symmetric, and transitive. The accessibility relation does not have to have these qualities; there are certainly other choices possible, such as those used when modeling belief rather than knowledge. The properties of knowledge Assuming that is an equivalence relation, and that the agents are perfect reasoners, a few properties of knowledge can be derived. The properties listed here are often known as the "S5 Properties," for reasons described in the Axiom Systems section below. The distribution axiom This axiom is traditionally known as K. In epistemic terms, it states that if an agent knows and knows that , then the agent must also know . So, This axiom is valid on any frame in relational semantics. This axiom logically establishes modus ponens as a rule of inference