Kripke Structure

释义 Definition

Kripke structure（克里普克结构）：形式化方法与模型检测中常用的一种状态转移模型，通常由一组状态、状态之间的转移关系、以及给每个状态标注的原子命题真值组成，用来描述系统“可能如何演化”以及在不同状态下“哪些性质成立”。（在模态逻辑中也常用于给公式提供语义解释。）

发音 Pronunciation (IPA)

/ˈkrɪpki ˈstrʌktʃər/

例句 Examples

A Kripke structure can model a simple traffic light.
克里普克结构可以用来建模一个简单的交通信号灯系统。

We verified the safety property by checking the temporal logic formula against the system’s Kripke structure.
我们通过将时序逻辑公式与系统的克里普克结构进行核对来验证安全性质。

词源 Etymology

“Kripke”来自美国哲学家与逻辑学家 Saul Kripke（索尔·克里普克） 的姓氏。相关语义模型最早用于模态逻辑（modal logic）的语义解释，后来在计算机科学中被广泛采用，用作模型检测（model checking）里描述程序/系统行为的基础结构。“structure”表示“结构、构造”。

相关词 Related Words

• Model
• State
• Transition
• Labeling
• Atomic Proposition
• Modal Logic
• Temporal Logic
• Model Checking
• LTL
• CTL

文献与作品 Literary Works

• Saul Kripke, “Semantical Considerations on Modal Logic”（1963）
• Edmund M. Clarke, Orna Grumberg, Doron A. Peled, **Model Checking**（1999）
• Christel Baier, Joost-Pieter Katoen, **Principles of Model Checking**（2008）
• _Handbook of Model Checking_（Springer, 2018）