跳转到内容

克里普克结构

维基百科,自由的百科全书
本文介绍了在模型检测中使用的克里普克结构。对于更一般介绍,请参见克里普克语义'。

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

形式化定义

[编辑]

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

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

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

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

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

例子

[编辑]

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

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

  • S = {s1, s2, s3}
  • I = {s1}
  • R = {(s1, s2), (s2,s1), (s2,s3), (s3、s3)}
  • L = {(s1, {p、q}), (s2, {q}), (s3, {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.