More rules
Until now we have only implemented the modal logic system K. For epistemic logic other systems are used, for example system S5 where the relations in the models are equivalence relations. These extended systems can be built from system K by adding more rules.
Rule D, seriality
If a model is serial all worlds have at least one outgoing relation (for each agent), so it can not be the case that M,s ⊨ □i ⊥. An equivalent statement is that if M,s ⊨ □i φ then also M,s ⊨ ◇i φ; if φ holds everywhere then it must hold somewhere.
We can add this last formulation as a rule.
The D- rule is just the contrapositive of the D+ rule. Also remember that we make copies of the conclusion with the +C meta-rule, so both the D- and the □- rule can be applied to the same formula.
Rule T, reflexivity
In a reflexive model if □i φ holds in some world then φ also holds in that world itself, since there is a relation to it. Conversely, if we know that φ holds in some world, then in that world ◇i φ also holds.
As a rule
All reflexive models are also serial, so we could still use rule D for this class of models. But that is just a waste of resources, since rule T alone suffices.
Rule 4, transitivity
Models where all relations are transitive are more interesting. Transitivity can be formulated as: If in all reachable worlds φ holds, and a world [Δ]i is reachable, then φ also holds in that world.
Rule 5, euclidean
Finaly models with euclidean relations are very similar,
Mixing
Instead of adding these extra rules for all agents we could restrict each rule to a subset of them. That way we obtain a kind of mixed system.
A mixed system can be very useful for modeling many problems. Take the muddy children problem. The knowledge of the children can be modeled using system S5, as is common in epistemic logic. Then an extra modal operator can be introduced for the announcement “At least one of you is muddy”. This operator will not follow the rules of S5, the situation after two announcements differs from that after just one, so the relation is clearly not transitive. In fact system K looks to be best suited for this time step operator.