线性时间性质
线性时间行为
为了分析由迁移系统表示的系统,可以采用基于状态或基于动作的方法。现在我们关注基于状态的方法。所以我们暂时忽略迁移的动作标记,而用状态的原子命题来精确地表征系统性质。
我们的验证算法将在迁移系统的状态图中进行,这里状态图是迁移系统删去动作标记后得到的有向图。记迁移系统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