线性时间性质

线性时间行为
为了分析由迁移系统表示的系统，可以采用基于状态或基于动作的方法。现在我们关注基于状态的方法。所以我们暂时忽略迁移的动作标记，而用状态的原子命题来精确地表征系统性质。

我们的验证算法将在迁移系统的状态图中进行，这里状态图是迁移系统删去动作标记后得到的有向图。记迁移系统TS的状态图为G(TS).

令\(Post^*(s)\)表示状态图\(G(TS)\)从s开始可达的状态(一步或多步)，并推广到S的子集C: \(Post^*(C)=\cup_{s\in C} Post^*(s).\) 类似定义\(Pre^*.\)

我们将用路径刻画状态图的性质。下面给出一些定义。
TS的路径片段是一个状态序列，有限路径片段记作\(\hat{\pi}=s_0\cdots s_n \), 无限路径片段记作\(\pi = s_0s_1\cdots,\) 都满足\(s_i\in Post(s_{i-1}).\)
用\(\pi[j]=s_j\)表示第j个状态，从0开始计数。设\(\pi[..j],\pi[j..]\)分别表示其前缀、后缀（均包括\(\pi[j]\)）。用\(last(\pi), len(\pi)\)分别表示其末项及长度。

与TS的执行片段类似，我们定义极大路径片段为无穷序列或以终止状态结束的状态片段，定义起始路径片段为\(s_0\in I\)的路径片段。对于取定的状态s，定义Paths(s)为s起始的极大状态片段，\(Paths_{fin}(s)\)表示其中的有限路径片段。
最后，TS的路径定义为起始极大路径片段，用Paths(TS)表示。\(Paths_{fin}(TS)\)表示其中的有限路径。

我们通过观察状态上的原子命题来研究迁移系统的性质。
设TS是没有终止状态的迁移系统，则路径片段的迹\(trace(\pi)\)定义为将\(\pi\)中的s替换为L(s)得到的序列。类似定义Traces(s), Traces(TS).

原子命题集合AP上的线性时间性质(LT)是\((2^{AP})^{\omega}\)的子集。
若P是AP上的LT性质，\(Traces(TS)\subseteq P\)，称TS满足P，记作\(TS\vDash P.\) 类似定义状态\(s\vDash P.\)

定理. 设TS, TS'都是无终止状态的迁移系统，且具有相同的命题集合AP。则以下两个命题等价：
(1) \(Traces(TS)\subseteq Traces(TS')\).
(2) 对任意AP上的LT性质P，\(TS'\vDash P \Rightarrow TS\vDash P.\)
命题(1)中的包含关系可以视为"TS是TS'的正确实现"。

安全性质与不变式
安全性质可以通俗讲为“坏事不发生”。典型的安全性质包括互斥性，无死锁性。

以上的例子是一类特殊的安全性质：不变式。不变式是由状态的条件给出的LT性质，使得对所有可达状态成立。即存在命题逻辑\(\Phi\)，使得\(\forall s\in Reach(TS),L(s)\vDash \Phi.\)
对于可达状态集有限的系统TS，可以采用深度优先(DFS)或广度优先(BFS)的算法来检验不变式。

安全性质\(P_{safe}\)定义为AP上满足一下条件的LT性质：使P不成立的任何无限单词，都包含一个坏前缀。坏前缀是指"坏事已经发生"的有限前缀\(\hat\pi\)，记作\(BadPref(P_{safe})\). 因此，以该前缀开始的无限单词都不可能满足P。极小坏前缀是指其任何一个真前缀都不是坏前缀的坏前缀。
任何不变式都是安全性质。

安全性质是对有限迹的要求，即\[TS\vDash P_{safe} \Leftrightarrow Traces_{fin}(TS)\cap BadPref(P_{safe})=\emptyset.\]
定理. 设TS, TS'不包含终止状态，且具有相同的命题集AP。以下命题等价：
(a) \(Traces_{fin}(TS)\subseteq Traces_{fin}(TS').\)
(b) \(\forall P_{safe}, TS'\vDash P_{safe} \rightarrow TS\vDash P_{safe}.\)
注意，有限迹包含与迹包含是不同的条件，有限迹包含要稍弱一些。如果TS'有限，TS无终止状态，则TS迹包含与TS'与有限迹包含等价。

活性性质
活性性质是对安全性质的补充。只要算法不做任何事情，坏事一定不发生，这不是我们想要的算法。活性性质的直观意义是“好事终将发生”。活性性质不约束有限行为，但对无限行为提出要求。

形式化描述为，如果LT性质P满足\(pref(P)=(2^{AP})^*\),称性质\(P=P_{live}\)为活性性质，这里pref(P)表示P的有限前缀组成的集合。换言之，P是活性性质当且仅当对任意有限单词\(\sigma\)，都存在无限单词\(\omega\)使得\(\sigma\omega\in P.\)

典型的活性性质包括"终将"、"终将重复"、"无饥饿(\(wait\to crit\))"等。

安全性质与活性性质的关系
(1) 不存在非平凡LT性质P，使P既是安全性质又是活性性质。
(2) 每个AP上的LT性质P，均存在一组\(P_{safe},P_{live}\)使得\[P=P_{safe}\cap P_{live}.\]
公平性
公平性约束排除了被认为不实际的无限行为。有几种常见的公平性约束：
(1) 无条件公平性：每个进程都无限次运行；
(2) 强公平性：无限次激活的进程都无限次运行；
(3) 弱公平性：从某时刻起持续激活的进程都无限次运行。
这里激活可以理解为迁移条件成立，而运行可以理解为迁移的执行。蕴含关系为靠前的公平性蕴含了后者。
如果迁移系统TS的所有F公平的路径满足LT性质P，称TS在公平性假设F下满足性质P，记作\(TS\vDash_F P\).

公平性与安全性
如果迁移系统TS的任何一个可达状态s，都存在满足公平性假设F的一个执行片段以s开始，则称F对TS是可实现的。这就意味着可以把TS的每个起始有限执行片段扩充为一个F公平执行。

定理. 设F是对迁移系统TS的可实现的公平性假设，\(P_{safe}\)是AP上的安全性质，则\[TS\vDash P_{safe}\Leftrightarrow TS\vDash_F P_{safe}.\]

    所属分类：Formal Methods     发表于2022-02-09