线性时序逻辑
线性时序逻辑（，LTL），或称线性时态逻辑，是一种模态时态逻辑。其时态运算符限定于描述从一个给定的状态开始的某一条路径上的事件。线性时序逻辑由阿米尔·伯努利在1977年提出。线性时序逻辑和两者可以归入更广义的中。 语法和语义 一个线性时序逻辑公式由以下三种要素构成： ψ W φ ≡ (ψ U φ) ∨ G ψ ≡ ψ U (φ ∨ G ψ) ≡ φ R (φ ∨ ψ) ψ M φ ≡ ¬(¬ψ W ¬φ) ≡ (ψ R φ) ∧ F ψ…
标签：#模型檢查
共 3 篇文章
模型检测
在计算机科学领域，模型检测或属性检测是一种用于验证系统的有限状态模型是否满足给定规范（即正确性）的方法。这种方法通常应用于硬件或软件系统；在此类系统中，规范不仅包含安全性需求（例如避免导致系统崩溃的状态），同时也包含活性需求（例如避免活锁现象）。 为了能够通过算法解决此类问题，系统的模型及其规范均需使用精确的数学语言进行形式化表述。为此，该问题被转化为逻辑范畴下的任务，即验证某个特定的结构是否满足给定的逻辑公式。这一通用概念适用于多种逻…
克里普克结构
: 本文介绍了在模型检测中使用的克里普克结构。对于更一般介绍，请参见克里普克语义'。 克里普克结构（或称Kripke结构）是迁移系统的一个变种，最初由索尔·克里普克提出，用于在模型检测中表示一个系统的行为。克里普克结构本身是一个图，其结点表示系统可达的状态，其边表示状态的迁移。 有一个标号函数将结点与结点所具有的性质的集合映射起来。时序逻辑传统上是由克里普克结构进行解释的。 形式化定义 设 AP 为 原子命题 的集合，比如：包含变量、常…