Kripke 结构 | Codeboy's Blog

形式陈述

Kripke 结构写作

K=(S,I,R,AP,L),

其中 $S$ 是状态集合， $I\subseteq S$ 是初始状态集合， $R\subseteq S\times S$ 是转移关系， $AP$ 是原子命题集合，标记函数

L:S\to 2^{AP}

给出当前状态中为真的原子命题，因此 $K,s\models p$ 当且仅当 $p\in L(s)$ 。命题逻辑的布尔组合仍在这个当前赋值上递归求值，例如

K,s\models\neg\varphi\iff K,s\not\models\varphi, \qquad K,s\models\varphi\land\psi \iff K,s\models\varphi\text{ 且 }K,s\models\psi.

Kripke 结构比单个命题赋值多出转移关系，使逻辑可以量化未来路径。对 $\pi=s_0s_1\cdots$ ，状态词

L(\pi)=L(s_0)L(s_1)\cdots

保留命题观察，却遗忘产生相同标记序列的具体状态身份。与标号转移系统相比，LTS 把动作放在边上，Kripke 结构把逻辑事实放在节点上。通过增加中间状态可以把边动作编码成命题，但这会增加状态并改变一步粒度；两种标记位置不能视为零成本互换。

从状态 $s$ 出发的无限路径是序列

\pi=s_0s_1s_2\cdots, \qquad s_0=s,\quad (s_i,s_{i+1})\in R.

许多 CTL、CTL* 和经典 LTL 模型检查教材要求 $R$ total，即每个状态至少有一个后继。真实终止状态可加自环并永久保持标记，也可改用明确的有限轨迹语义；两种选择对 next 与最终性公式可能给出不同结果，必须在满足定义前声明。

初始集合可以含多个状态，用来表示未知输入或环境初始选择。判断整个系统满足状态公式 $\varphi$ ，通常要求

\forall s_0\in I,\qquad K,s_0\models\varphi.

只检查一个方便状态不能替代上述全称量词。公平性也不是五元组的隐含成分：若只量化公平路径，应另给 $Fair\subseteq Paths(K)$ 或等价接受条件，并明确把路径域限制到 $Fair$ 。无声明地删除“不喜欢”的无限路径会改变满足结论。

直觉

令每个进程位置属于 $\{N,T,C\}$ ，分别表示非临界区、尝试进入和临界区。状态写作 $(\ell_1,\ell_2)$ ，原子命题 $c_1,c_2$ 分别在 $\ell_1=C$ 、 $\ell_2=C$ 时为真。

若模型错误地允许两个进程从 $(T,T)$ 各自独立进入临界区，就会出现路径

(N,N)\to(T,N)\to(T,T)\to(C,T)\to(C,C).

在末状态有 $L(C,C)=\{c_1,c_2\}$ ，违反状态断言 $\neg(c_1\land c_2)$ 。若协议正确，转移关系应排除所有通向双临界状态的路径，而不是只把 $c_1\land c_2$ 从标记中删掉；标记必须忠实描述状态，不能用来掩饰行为。

“每个尝试进程最终进入临界区”还需要观察整条路径，并通常依赖调度公平性。状态图没有坏状态只能证明互斥安全性，不能由此推出无饥饿。

例子与边界

取

S=\{s,u,v\},\quad I=\{s\},

R=\{(s,u),(s,v),(u,u),(v,v)\},

并令 $L(u)=\{success\}$ 、 $L(v)=\{retry\}$ 、 $L(s)=\varnothing$ 。从 $s$ 有两条基本无限路径

su^\omega \qquad\text{和}\qquad sv^\omega.

前一条在一步后到达 success，后一条永远没有 success。因此 $K,s\models EF\,success$ ，却有 $K,s\not\models AF\,success$ 。三个状态和四条边即可手工复核存在与全称路径量词的差别。

这正是分支时序语义需要保留的结构。若只列出一条样例执行，存在量词看似得到见证，却完全没有检查其他分支；若把所有未来先压成一个动作集合，分支选择发生在何时也会丢失。

CTL 把路径量词 $A/E$ 与时间算子组合成状态公式，LTL 则在单条路径上解释公式，再由模型满足关系对初始路径作全称约定。二者共享 Kripke 状态图，却有不同语法层次。

推论与应用

模态逻辑和直觉主义逻辑也使用称为 Kripke frame/model 的结构，但可达关系、单调赋值和满足关系的条件随逻辑而变。本页的对象专指并发系统模型检查中带状态标记的转移结构，不是“一阶模型论中的任意结构”的总称。

Kripke 结构也不含转移概率。若从状态出发的多条边带概率，需要 Markov 链或 MDP；把非确定分支平均分配概率会擅自改变系统语义。

有限 Kripke 结构可显式枚举，状态由多个变量组合时却可能指数增长。模型检查问题规定如何判定 $K\models\varphi$ ，符号模型检查则用逻辑表示状态集合，而不是逐个存储节点。

参考资料

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999, Ch. 2。
Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, §§2.1, 3.1, 6.1。
Michael Huth and Mark Ryan, Logic in Computer Science, 2nd ed., Cambridge University Press, 2004, Chs. 3–4。