克里普克结构

本文介绍了在模型检测中使用的克里普克结构。对于更一般介绍，请参见克里普克语义'。

克里普克结构（或称Kripke结构）是迁移系统的一个变种，最初由索尔·克里普克^[1]提出，用于在模型检测^[2]中表示一个系统的行为。克里普克结构本身是一个图，其结点表示系统可达的状态，其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。^{[來源請求]}

形式化定义

设 AP 为 原子命题 的集合，比如：包含变量、常量和谓词符号的布尔表达式。 Clarke et al.^[3] 将一个定义在 AP 上的克里普克结构定义为一个四元组 M =(S, I, R, L)，其中：

• 一个有限状态集合 S.
• 一个初始状态集合 I ⊆ S.
• 一个迁移关系 R ⊆ S × S ，其中 R 是一个左部满射的多值函数，即∀s ∈ S ∃s' ∈ S 使得 (s,s') ∈ R.
• 一个标号函数（或称“解释函数”） L: S →2^AP.

由于R 是一个多值函数，因此通过克里普克结构，总是能够构建一个无穷路径。死锁状态可以建模为仅存在一条指向自身的的出边。标号函数 L 定义为：对于每个状态 s ∈ S，L(s) 表示所有在 s 中有效的原子命题构成的集合。

克里普克结构 M 中的一条 路径 是指一个状态序列 ρ = s_1, s_2, s_3, ...，其中，对于每个 i > 0，存在关系 R(s_i, s_i+1) 。路径 ρ 上的 单词 是指一个原子命题集合的序列 w=L(s₁),L(s₂),L(s₃),...，也就是定义在字母表2^AP上的一个 ω单词 。

由这一定义，仅包含一个初始状态 i ∈ I 的一个Kripke结构可以通过一个单例输入字母表被一个摩尔型有限状态机识别，同时其输出函数为克里普克结构的标号函数。^[4]

例子

设原子命题集合 AP ={p, q}。 p和q可以模任意可以由克里普克结构建模的系统中的布尔命题。

右图表示了一个克里普克结构 M =(S, I, R, L)，其中：

• S = {s₁, s₂, s₃}
• I = {s₁}
• R = {(s₁, s₂), (s₂,s₁), (s₂,s₃), (s₃、s₃)}
• L = {(s₁, {p、q}), (s₂, {q}), (s₃, {p})}

M 可能产生一条路径 ρ = s1,s2,s1,s2,s3,s3,s3,... 以及一个单词 w = {p,q},{q},{p,q},{q},{p},{p},{p},...，其中 w 是执行路径 ρ 对应的单词。 M 可以产生属于语言 ({p, q}{q})*({p})^ω∪({p, q}{q})^ω 的执行路径。

与其他表示方式的关系

尽管这一术语被普遍使用于模型检测社区，一些模型检测的教科书上并没有（或者实际上并没有）以这种扩展的方式定义克里普克结构，而只是简单使用了“（带标号的）迁移系统”的概念，同时添加了一个包含原子命题 AP 集合的动作的集合 Act 。于是，迁移关系因此被定义为 S × Act × S 集合的子集，标号函数 L （L 如上文定义）即对应于动作集合 Act。在这种定义方法中，通过抽取动作标签而得到的二元关系被称为状态图。^[5]

Clarke et al. 重新定义了克里普克结构为一个转换集合（而不仅仅是一个转换）。当定义了模型μ-演算的语义时，转换集合等价于上文中的标号迁移。

参见

• 时间逻辑
• 模型检测
• 克里普克语义
• 线性时序逻辑
• 计算树逻辑

参考文献

1. Kripke, Saul, 1963, “Semantical Considerations on Modal Logic,” Acta Philosophica Fennica, 16: 83-94
2. Clarke, Edmund M. (2008): The Birth of Model Checking. in: Grumberg, Orna and Veith, Helmut eds.: 25 Years of Model Checking, Vol. 5000: Lecture Notes in Computer Science.
3. Clarke, Grumberg and Peled: "Model Checking", page 14.
4. Klaus Schneider. Verification of reactive systems: formal methods and algorithms. Springer. 2004: 45. ISBN 978-3-540-00296-3. 
5. Christel Baier; Joost-Pieter Katoen. Principles of model checking. The MIT Press. : 20–21 and 94–95. ISBN 978-0-262-02649-9.