Specifying Systems 笔记 (Liveness)

Specifying Systems 的 1-7 章层层推进，在实例中穿插着原理讲解，深入浅出地讲解了 Specification 是什么，以及如何设计系统规约。这些 Specification 表明了系统的 Safety 属性 —— 即系统行为被约束在一定范围内，不会做出一些不被允许的行为（something bad does not happen）。在 TLA+ 中，通常使用公式 来描述系统的 Safety 属性（约束）。Safety 属性说明了系统中什么不能发生，但无法表达系统中某些时间一定会发生的这类属性，而 Liveness 便可以表达（“something good eventully happen”）。Liveness 使用时态逻辑公式进行描述，一个系统规约可以通过公式 来同时描述其对 Safety 和 Liveness 的要求，公式末尾的 便是描述 Liveness 属性的公式。

一些概念

value

value 表示通常意义上的值，如 。TLA+ 的语义基于 ZF 集合论，因此其 value 只是集合（set）的另一个称呼。

state

state 是对一些变量进行赋值（的结果），如 、 等。

state function

state function 是一个以 变量（不包含 primed variable）、常量、操作符构建的表达式。这个表达式给所有 state 都映射了一个 value。可以理解为每个 state 都可以经过这个 function 计算，得到一个 value。

state predicate

结果 value 为 Boolean 类型的 state function。即 state predicate 一个作用于 state 进行真值判断的公式。

behavior

behavior 是 state 组成的无穷序列，如 。需要注意的是，一个系统可能有多个 behavior，比如并发系统可能有多种执行顺序，产生不同的 behavior。

step

step 是 state 之间直接变化的步骤。假如 、 分别是两个相邻的 state，那么 就是表示 从 直接变化到 的 step，无论 state 中有多少个变量，这个变化都是原子的，不会产生其它中间状态。

primed variable

变量发生变化后的值，如 表示 hr 变量经过一个 step 之后，其值等于原先的值加 1。

action

包含 primed variable 和 unprimed variable 的 formula。action 作用于 step 进行真值判断，以断定 state（的 value）是否可以再发生变化。specification（规约）通常由许多 action 组成。

formula

值为 TRUE 或 FALSE 的逻辑表达式（数理逻辑中的「公式」）

---

这些定义的形式和语义都不一定准确，只是帮助加深理解 TLA+。精确定义详见 Specifying Systems，尤其是 Chapter 16 有许多描述。

逻辑基础

命题逻辑

命题逻辑语法可以用如下 BNF 表示：

谓词逻辑

PTL: Propositional Temporal Logic，是 LTL 的另一种简称，参考：

• https://en.wikipedia.org/wiki/Linear_temporal_logic
• http://discuss.tlapl.us/msg00894.html

Temporal Logic 简介

时态公式是行为（behavior）的真值判断式。对于一个行为 ，以及一个时态公式 ，如果 满足 ，则可以表示为：

也可称作时态公式 对于行为 是真的，或称行为 满足公式 。

公式可以通过连接词进行组合，也可使用量词进行修饰。组合公式的含义如下：

上面出现的公式 、 都未加定义，通常由如下三种形式的公式组成:

• state predicate，P 是一个「状态谓词」。其语义是：如果将 看作时态公式，那么 （behavior）满足 当且仅当 中的第一个 state 满足 。

• 其中 是 state predicate。behavior 满足 当且仅当 behavior 中所有 state 满足 。

• 其中 是 action， 是 state function。behavior 满足该公式 当且仅当 behavior 中每一对相继的 states 是一个满足 的 step。

  注意： 中的 可以是 state function，并不限定于 variables（如 )。state function 可以增加 prime 运算符形成 transition function。 等价于 。详见 Spcifying Systems 16.2.3。

这三种公式中，虽然 是一个 state predicate，但可以将其看作是一个没有 primed variables 的 action（这种 action 作用于 state 得到新的 state' 没有改变，即一个 stuttering step）。这样，我们就可以把时态公式归纳为两种形式： 和 ，其中 是一个 action。

语义解释

定义 是 的第 个 state， 即是: 。注意这里的自然语言表述，第一个 state 是 ， 是第一（）个 state。

为 true 等价于 是一个 step。特殊场景：如果 是一个 state predicate，只要 对于第一个状态（）判定为 true， 就是一个 step。

为 true 等价于 所有的 step（）都是一个 step。

定义：，因此 是 的第一个 step。 为 true 等价于 对于所有的 ， 为 true：

一个很自然的泛化就是把 action 换成 formula ：

示例：

更多时态公式定义

• 公式中 A 是一个 action， 是一个 state function，这表示最终某些 step 是一个改变了 且满足 的 step。

  如果定义 ，那么也可以理解 是 和 的结合，即最终有一个 step 会发生。（这种理解不是完全正确的，因为 并不是一个合法的公式，只是一个简写）。

• 太好理解，不用解释

• 太好理解，不用解释

时态逻辑重言式（恒等式）

时态逻辑推理规则（类似于 MP 规则）

• 概括（泛化？）规则：，表示 为 true 时， 为 true。
• 蕴含概括规则：

需要意与重言式与推理规则的区别。例如，上面的’概括规则’要求 为 true 时才能推定 ，但重言式没有这个要求，因为重言式的语义是永真的。

Liveness 定义

liveness 属性可以通过时态逻辑进行描述！

TLA+ 提供两种标准的（常用的）构建 Liveness 的符号

Weak Fairness

这些公式的等价性可以通过时态逻辑和命题逻辑的重言式进行证明。如果用 表示 ，用 表示 。则可以将 可表示为 。

Strong Fairness