K系统

和命题逻辑的树形图方法类似。不过在每个命题旁边要标准一个自然数，表示某个可能世界。和命题逻辑相比，多了下面四条规则：

 在第四个规则中，irj的j必须在前面没有出现过。

例1：用树形图验证：

例2：用树形图验证⊨ (◇p∧◇﹁q)→◇□◇p是否成立。

树形图没有封闭，所以(◇p∧◇﹁q)→◇□◇p不是有效式。从树形图中可以读出反模型：

其他正规系统

在框架上加一些限制条件，比如自返性、对称性、传递性、持续性。

自返性r：对任意的w，Rww

对称性s：如果Rwu，则Ruw

传递性t：如果Rwu且Ruv，则Rwv

持续性h：对任意的w，存在v，Rwv

在用树形图判定模态命题在这些系统中是否是有效式时，需要添加一些规则：

S5系统

在K_V 中R是全通关系，即任意的u和v，Ruv。所以它的树形图比较简单，r无需出现。

所以可以用上述方法验证S5系统的有效式。