Kripke结构是过渡系统的变体，最初由Saul Kripke提出，用于模型检查来表示系统的行为。 它基本上是一个图，其节点表示系统的可达状态，其边表示状态转换。 标记函数将每个节点映射到一组保持在相应状态的属性。 时间逻辑传统上用Kripke结构来解释。

正式定义设AP是一组原子命题，即对变量，常量和谓词符号的布尔表达式。 Clarke等人[3]在AP上定义Kripke结构为4元组M =（S，I，R，L）由...组成
一组有限的状态S.
一组初始状态I⊆S.
过渡关系R⊆S×S使得R是左总的，即∀s∈S∃s'∈S使得（s，s'）∈R。
标签（或解释）功能L：S→2AP。

由于R是左总数，因此总是可以通过Kripke结构构建无限路径。死锁状态可以通过单个传出边缘建模回自身。标记函数L为每个状态s∈S定义在s中有效的所有原子命题的集合L（s）。

结构M的路径是状态序列ρ= s1，s2，s3 ......，使得对于每个i> 0，R（si，si + 1）成立。路径ρ上的单词是一系列原子命题的集合w = L（s1），L（s2），L（s3），...，它是字母表2AP上的ω-字。

根据这个定义，Kripke结构（例如，只有一个初始状态i∈I）可以用具有单例输入字母表的Moore机器识别，并且输出函数是其标记函数。

与其他概念的关系尽管这个术语在模型检查社区中很普遍，但是一些关于模型检查的教科书没有以这种扩展的方式定义“Kripke结构”（或者根本没有1），而只是使用（标记的）过渡系统的概念， 有一套行动法，过渡关系被定义为S×Act×S的一个子集，它们还扩展到包括一组原子命题和状态的标记函数（如上定义的L）。 在这种方法中，通过抽象出动作标签获得的二元关系称为状态图。

Clarke等人。 将Kripke结构重新定义为一组过渡（而不仅仅是一个），当它们定义模态μ演算的语义时，它等同于上面标记的过渡。

本词条内容贡献者为:

李嘉骞 - 博士 - 同济大学