克里普克结构维基百科,自由的 encyclopedia 克里普克结构(或称Kripke结构)是迁移系统的一个变种,最初由索尔·克里普克[1]提出,用于在模型检测[2]中表示一个系统的行为。克里普克结构本身是一个图,其结点表示系统可达的状态,其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。[来源请求] 本文介绍了在模型检测中使用的克里普克结构。对于更一般介绍,请参见克里普克语义'。
克里普克结构(或称Kripke结构)是迁移系统的一个变种,最初由索尔·克里普克[1]提出,用于在模型检测[2]中表示一个系统的行为。克里普克结构本身是一个图,其结点表示系统可达的状态,其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。[来源请求] 本文介绍了在模型检测中使用的克里普克结构。对于更一般介绍,请参见克里普克语义'。