Program Verification 02 - Linear Temporal Logic (unfinished)
# 前置知识
在阅读本文档前,请确保你已掌握布尔逻辑的基础知识,详见 Program Verification 知识板块中的 01 - Basic Logic 文档。
在阅读本文档前,请确保你已掌握有限状态自动机的相关知识。详情请自学编译原理,暂无相关文档,敬请谅解。
# 基本概念
在古典逻辑(包括命题逻辑和谓词逻辑)中,逻辑公式是基于逻辑公理和状态进行演算的:对于给定的状态,我们能对逻辑公式的真值进行推断,非真即假。例如,“今天是星期一”要么是真、要么是假。
时态逻辑 (temporal logic) 在谓词逻辑的基础上引入了“时间”的概念,并扩展了一组时态操作符,用于动态地描述逻辑真值。例如,“今天是星期一”可能在当前时刻为真,但在下一时刻为假。
而 线性时态逻辑 (linear temporal logic, LTL) 指的就是使用线性时间轴的时态逻辑。在 LTL 中,每个时刻都有至多一个前继和后继时刻。
如果说古典逻辑是在单一时刻下的、静态的逻辑,那么时态逻辑就是涵盖了多个时刻的、动态的逻辑。具体地讲,时态逻辑在谓词逻辑的基础上:
建立时间轴,描述不同时刻之间的可达性关系。
扩展时态运算符,描述能涵盖多个时刻的逻辑公式,并推断其在给定时刻下的真值。
需要注意的是,时态逻辑公式描述的是相对的时刻关系而非绝对时刻,形如“ 在下一时刻成立”或“ 在 成立之后成立”,而不是“ 在时刻 成立”。绝对时刻由状态对谓词的满足来描述。
# 时态运算符
# 基本语法
下列术语中出现的运算符统称为 时态运算符 (temporal operators) 。
表示 LTL 公式 (LTL formula) , 表示 原子命题 (atomic proposition) , 或 表示真和假。
neXt : 或 表示 在 下一时刻 (the next moment) 为真。
Globally : 或 表示 在 未来所有时刻 (all future moments) 为真。
Finally : 或 表示 在 未来某些时刻 (some future moments) 为真,或者说未来 终究 (eventually) 会为真。
每个一元时态运算符都有其对应的 past operators : 表示上一时刻, 表示过去所有时刻, 表示过去某些时刻。
Until : 表示 至少直到 (at least until) 为真之前都为真。这蕴涵了 的事实。注意,这不表示在 为真之后 一定为假。
Weak until : 表示 至少直到 为真之前都为真,但 可以永不为真,即 可以永真。
Release :没看懂。声称 ϕRψ = ¬(¬ϕU¬ψ) ,但是这不是 ϕRψ = ψUϕ 吗?
- ϕRψ holds for a word if ψ always holds, a requirement that is released as soon as ϕ becomes valid
# 组合
组合 和 运算符能够描述新的、更复杂的时态:
等价于 ,意为在无限长的时间里 总是在未来有机会被满足。
等价于 ,意为从未来某个时刻开始, 将从那时起保持为真。
所有的时态运算符都可以用 和 运算符来描述:
# 逻辑等价性质
对偶律 (duality law) :
幂等律 (idempotency law) :
吸收律 (absorption law) :
分配律 (distributive law) :
expansion law :
# 时态模型
# Kriple Structure
定义 Kriple structure 为一个四元组 ,其中:
是有限的状态集合, 是初始状态集合。
是状态之间的转换关系,每个转换关系使用可用的运算符之一来表示。
是一个状态标记函数,它标记了每个状态下所有原子命题是否成立,其中 为系统中原子命题的全集。
啊
# LTL 和计算机科学
LTL 可用于软件系统的形式化验证或 model checking ,在这种情况下,我们会将被测系统建模为一个 transition system ,记为 ,通常表示为有限状态机的形式。
TBD:LTL 时刻和被测系统的状态之间的区别和联系?
Safety: Something bad will never happen: 𝐺 ¬ 𝑏𝑎𝑑 If it fails to hold, it’s easy to produce a witnes
Liveness: Something good will eventually happen: 𝐹 𝑔𝑜𝑜𝑑 What does a witness for this look like?
# 时态语义
在计算机科学的 domain 下,古典逻辑扩展了状态的概念,基于状态描述谓词的可满足性。不同的是,LTL 公式的满足不是基于某一时刻或某些时刻的,而是基于路径或整个 transition system 的。
LTL formulae φ stands for properties of paths (Traces) and The path can be either fulfill the LTL formula or not.
The semantics of φ is extended to an interpretation over paths and states of a TS.
Thus, a transition system TS satisfies the LT property P if all its traces respect P, i.e., if all its behaviors are admissible. A state satisfies P whenever all traces starting in this state fulfill P.
If all initial paths of TS paths starting in an initial state s0 ∈ I satisfy ϕ.
Thus, it is possible that a TS (or si) satisfies neither ϕ nor ¬ϕ
Any LTL formula can be transformed into a canonical form, the so-called positive normal form (PNF). In order to transform any LTL formula into PNF, for each operator, a dual operator needs to be incorporated into the syntax of PNF formulae.
# Büchi 自动机
Büchi 自动机 (Büchi automaton) 是一种有限状态自动机,记为 ,其中:
为有限的状态集合, 为有限的字母表。
为 transition relation 。
为初始状态集合。
为接受状态集合。
Büchi 自动机的输入是无限长的序列,记为 。设 是一个 Büchi 自动机, 是 的一个输入,则:
定义 在 上的一次执行为一个无限长的序列,记为 ,其中 , , 。
称 接受 ,当且仅当存在 在 上的某个执行 ,满足 。也就是说,当且仅当执行 无限次地访问了某些接受状态,我们才认为 接受 。
TBD:samples from here (opens new window)
# 参考资料
Colorado State University, CS614 : Ch5-Summary.pdf (opens new window)
Brandeis University, CS112 : LTL-Artale-Slides.pdf (opens new window)
Sharif University of Technology, CE665-1 : Ch5-Linear Temporal Logic.pdf (opens new window)
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01