可达关系

可达关系决定一个世界在判断“必然”或“可能”时需要查看哪些世界。$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)$ 后，两条两步链 $aRbRd$ 与 $aRcRd$ 都有了对应的直接边。图中没有其他两步链，因此新关系已经传递。

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

可达关系的具体解释由模型给出：程序模型可用边表示执行步骤，知识模型可用边表示尚未排除的情形。普通二元关系记录哪些世界相连；需要概率或耗时的应用，还可为边配置相应的数据。

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$ 边往返匹配，过滤法则按有限公式集识别世界并把原关系压到商集上。两种构造都保留经过证明的模态信息，却不会保留任意图论性质，例如后继的精确数量。