Loading AI tools
克里普克结构（或称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 →2AP.
由于R 是一个多值函数，因此通过克里普克结构，总是能够构建一个无穷路径。死锁状态可以建模为仅存在一条指向自身的的出边。标号函数 L 定义为：对于每个状态 s ∈ S，L(s) 表示所有在 s 中有效的原子命题构成的集合。
克里普克结构 M 中的一条 路径 是指一个状态序列 ρ = s1, s2, s3, ...，其中，对于每个 i > 0，存在关系 R(si, si+1) 。路径 ρ 上的 单词 是指一个原子命题集合的序列 w=L(s1),L(s2),L(s3),...，也就是定义在字母表2AP上的一个 ω单词 。
由这一定义，仅包含一个初始状态 i ∈ 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. 重新定义了克里普克结构为一个转换集合（而不仅仅是一个转换）。当定义了模型μ-演算的语义时，转换集合等价于上文中的标号迁移。
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
