可达关系

可达关系决定一个世界在判断“必然”或“可能”时需要查看哪些世界。$wRv$ 可以读成“在 $w$ 看来，$v$ 是尚未排除的情形”“系统能从 $w$ 一步转到 $v$”，或者“信息状态 $v$ 延伸了 $w$”。真正固定的是量化方向：从 $w$ 出发检查 $R(w)$；故事性的解释必须服从这个方向，而不能反过来决定公式。

关系性质把不同故事压缩成可检验的结构约束。自反性表示当前世界也在自己的视野中；传递性表示二次可达不会增加一条全新的远端关系；串行性排除没有任何后继的死端。这些说法只描述视野的形状，还没有给命题真假赋值，因此不能仅凭一张关系图判断某个原子命题是否成立。

取 $W=\{a,b,c,d\}$，并令

于是 $R(a)=\{b,c\}$，$R(b)=R(c)=\{d\}$，而 $R(d)=\varnothing$。这个关系不串行，因为 $d$ 没有后继；不自反，因为没有 $(a,a)$；也不传递，因为 $aRb$ 且 $bRd$，却没有 $aRd$。若加入 $(a,d)$，只修复了这一条两步链，仍须逐一检查其他链，不能由一个补边例子断言整个关系传递。

这张图也展示 $R$ 与 $R^{\ast }$ 的差别：$d\in R^2(a)$，却不属于原来的 $R(a)$；在 $R^{\ast }$ 中，每个点还会因长度零路径而到达自身。若把程序的一次执行步骤解释为 $R$，那么“下一步都安全”与“此后每一步都安全”显然是两个不同条件。

“可达”不等于因果、概率或物理可行。关系可以是不对称的、含环的，甚至由建模者故意设成完全关系 $W\times W$。模态逻辑只从指定的边读取语义；若应用需要边权、发生概率或时间长度，必须把这些数据另行加入模型，普通可达关系不会替你保存它们。

Kripke 框架公理库Kripke 框架Kripke frame · Relational frame由非空世界集和其上可达关系组成、用于解释模态算子结构的语义框架。把非空世界集与可达关系配成 $(W,R)$，Kripke 模型公理库Kripke 模型Kripke model · Relational modal model在 Kripke 框架上为命题变量逐世界赋值而得到的模态语义模型。再加入命题赋值。对同一世界集改变 $R$，会改变 $\square$ 与 $◇$ 的量化范围，即使每个原子命题的赋值完全不变。

关系性质与模态公理之间存在精确对应：自反框架验证 $\square p\to p$，传递框架验证 $\square p\to ◻◻p$，串行框架验证 $\square p\to \diamond p$。这些对应不是把符号按外形配对；反向证明需要为关系性质的失败专门构造命题赋值，使相应公式在某个世界失效。

可达关系也支撑模型比较。模态互模拟公理库模态互模拟Modal bisimulation · Kripke bisimulation用原子一致与沿可达边的 forth、back 条件比较两个 Kripke 模型的模态行为。要求双方沿各自的 $R$ 边往返匹配，过滤法则按有限公式集识别世界并把原关系压到商集上。两种构造都保留经过证明的模态信息，却不会保留任意图论性质，例如后继的精确数量。