Kripke 结构

状态上的命题标记 ​

Kripke 结构写作

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

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

$$L:S\to 2^{AP}$$

给出每个状态中为真的原子命题。状态 $s$ 满足命题 $p$，正是 $p\in L(s)$。

它可以看作标号转移系统公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。的状态标记版本：LTS 把标签放在边上，Kripke 结构把逻辑可观察事实放在节点上。边动作可以通过增加中间状态编码成状态命题，状态标记也可附到 LTS 上；两种表示的转换会增加状态或改变一步的粒度，不能假装完全没有代价。

命题逻辑公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。只在单个赋值上判断布尔组合。Kripke 结构额外给出从当前状态可能延伸出的路径，使逻辑能够量化未来分支。

路径与 total 约定 ​

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

$$\pi =s_0{s}_1{s}_2\cdots ,s_0=s,(s_i,s_{i+1})\in R.$$

许多 CTL、CTL* 和经典 LTL 模型检查教材要求 $R$ 是 total 的：每个状态至少有一个后继。这样每个状态都有无限路径，时间算子不必另行定义在有限末端的行为。

真实程序可能终止。常见编码是在终止状态加入自环，让标记永久保持；另一做法是采用明确的有限轨迹语义。两者对 next 算子和“未来必有某事件”可能给出不同答案，模型必须说明采用哪一种。

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

$$\mathrm{\forall }{s}_0\in I,K,s_0\models \phi .$$

只检查一个方便的初始状态不能替代这个全称量词。

双进程互斥模型 ​

令每个进程位置属于 $\{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\}$，违反状态断言 $\mathrm{\neg }(c_1\wedge c_2)$。若协议正确，转移关系应排除所有通向双临界状态的路径，而不是只把 $c_1\wedge c_2$ 从标记中删掉；标记必须忠实描述状态，不能用来掩饰行为。

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

分支结构为何重要 ​

在状态 $s$，环境可能选择到 $u$ 或 $v$。从 $u$ 出发最终能到达 success，从 $v$ 出发却永远停在 retry。性质“存在一条路径最终成功”和“所有路径最终成功”在 $s$ 处答案不同：前者为真，后者为假。

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

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

与其他 Kripke 模型的边界 ​

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

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

有限 Kripke 结构可显式枚举，状态由多个变量组合时却可能指数增长。模型检查问题公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。规定如何判定 $K\models \phi$，符号模型检查则用逻辑表示状态集合，而不是逐个存储节点。

参考资料

• 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。