路径和状态图（Paths and State Graph）
- 状态图
- 路径
迹（trace）
刻画线性时间属性(LT Properties)
- 刻画基于信号量互斥系统的属性
- 刻画无饥饿(starvation freedom)系统的属性
安全性(Safety Properties)和不变性(Invariants)
- 不变性
- 安全性
闭包(Closure)
活性(liveness)
活性 VS 安全性

前面一直在讲怎么样去建模，讲述了KS，TS以及PG这三个模型，并用这几个模型建模了各类并发系统，接下来终于要到系统验证的第二步——specification，在这一步中，要为建立好的模型增加属性规范，为验证做好准备。本节主要研究TS的属性规范。

线性时间属性（Linear-Time Properties）指定了过渡系统应显示的轨迹。非正式地说，线性时间属性指定了所考虑系统的可允许（或期望）行为。

总的来说，刻画系统性质的目的就是规定系统可以出现哪些行为，排除那些不应该出现的行为。

除了线性时间(Linear-time)以外，还可以考虑分支时间(branching time)，分支时间等概念会在CTL里面讲到

路径和状态图（Paths and State Graph）

在看这部分内容之前，可以先回顾一下transition system那篇为文章下面的相关定义部分，很多概念都是相通的。

状态图

TS的状态图，用符号表示G(TS)，它是一个有向图定义为（V，E），V是vertices代表顶点，E是edge代表边，并且V=S，E={(s,s′)∈S×S∣s′∈Post(s)}\{(s,s')∈S×S|s'∈Post(s)\}{(s,s′)∈S×S∣s′∈Post(s)}

我们再次把自动售货机的张图片拿了出来，状态图就是把TS中的动作、AP等概念去掉，单纯的由状态和转换构成的有向图。

路径

TS上的有限路径片段(Path Fragment)π‾\overline{π}π定义为有限的状态序列，具体的：
π‾:s0s1...snsi∈Post(si−1)0<i≤n,n≥0\overline{π}:s_{0}s_{1}...s_{n} \\ s_{i}∈Post(s_{i-1}) \\ 0<i≤n,n≥0 π:s0s1...snsi∈Post(si−1)0<i≤n,n≥0

无限路径片段π定义为：
π:s0s1s2...si∈Post(si−1)i>0π:s_{0}s_{1}s_{2}... \\ s_{i} ∈ Post(s_{i−1}) \\ i>0 π:s0s1s2...si∈Post(si−1)i>0

最大(Maximal)路径片段定义为：
如果是有限路径片段，那么它结束于终止状态
或者该片段是一个无限路径片段

如果一个路径片段开始于初始状态，那么称为初始(Initial)路径片段

如果一个路径片段是初始、最大(maximal and initial)路径片段，那么它被称为TS的路径(Path)

我们记TS上的所有路径为Paths(TS)，Pathsfin(TS)Paths_{fin}(TS)Pathsfin(TS)是TS上所有初始、有限路径片段，记Paths(s)为从s状态开始的最大路径片段。

对比一下路径(path)和执行这两个概念(execute)，它们的定义和相关概念都是类似的，不过执行相比于路径多了动作转换

迹（trace）

经过前面的学习，我们知道了TS的路径(path)是系统上状态的序列(states sequence)
s0s1s2...s_{0}s_{1}s_{2}... s0s1s2...

而执行(execution)是系统上状态和动作的序列(states+actions sequence)
s0→α1s1→α2...s_{0}\xrightarrow{α_{1}}s_{1}\xrightarrow{α_{2}}... s0α1s1α2...

接下来，我们考虑一个由当前状态为真的原子命题组成的序列(sequences of sets of atomic proposition)，即L(s0)L(s1)L(s2)L(s3)...L(s_{0})L(s_{1})L(s_{2})L(s_{3})...L(s0)L(s1)L(s2)L(s3)...

我们称这类序列为迹(traces)

一个迹的实例就是把标签函数的求值表示出来，假如AP={a,b}，那么一个迹可能为∅{a}{a,b}{b}{b}∅...\varnothing \{a\}\{a,b\}\{b\}\{b\}\varnothing ...∅{a}{a,b}{b}{b}∅...

类似的来定义一下相关概念，Traces(s)代表从状态s开始的迹，Traces(TS)Traces(TS)Traces(TS)代表TS上初始迹的集合，Tracesfin(TS)Traces_{fin}(TS)Tracesfin(TS)代表TS上初始、有限迹的集合。

刻画线性时间属性(LT Properties)

因为线性时间属性（LT Properties）是TS中迹的要求，所以在AP上的线性时间属性是(2AP)w(2^{AP})^{w}(2AP)w的子集。

(2AP)w(2^{AP})^{w}(2AP)w表示的是AP中命题的无限级联的集合

如果AP={a,b}，那么(2AP)w(2^{AP})^{w}(2AP)w可以表示为
{{a}{a,b}∅...，{b}{a}∅∅...，...}\{ \{a\}\{a,b\}\varnothing...，\{b\}\{a\}\varnothing\varnothing...，... \}{{a}{a,b}∅...，{b}{a}∅∅...，...}

类似该集合中的元素，由无限个字符级联在一起组成的序列称为无限字(infinite word)，无限字可以表示为:
W=A0A1A2...W=A_{0}A_{1}A_{2}... W=A0A1A2...

当这个序列是有限时，便称为有限字(finite word)，有限字可以表示为:
W=A0A1A2...AnW=A_{0}A_{1}A_{2}...A_{n} W=A0A1A2...An

因为TS不考虑终止状态，所以也就无需使用有限字。

如果一个TS满足线性时间属性P，那么就表明：
TS⊨P当且仅当Traces(TS)⊆PTS \vDash P\text{ 当且仅当}Traces(TS) ⊆ P TS⊨P 当且仅当Traces(TS)⊆P

我个人的理解是线性时间属性P刻画了AP上能够出现的原子命题序列，而迹表示的是系统在AP上出现的原子命题序列，如果系统的迹是P的子集，那么肯定这个系统就满足了线性时间属性P。

刻画基于信号量互斥系统的属性

一说到信号量和互斥，再次搬出这个例子：

具体描述不再赘述，参看TS和PG建模并发系统

在这里，AP={crit1, crit2}，这个系统中的约束有一条：

“Always at most one process is in its critical section”

就是最多有一个进程能够进入临界区

用形式化的语言描述就是：
Pmutex=一个无限字的集合{A0A1A2...}且满足对于所有0≤i,{crit1,crit2}⊈AiP_{mutex} = 一个无限字的集合\{A0A1A2...\} 且满足对于所有0\le i,\{crit1, crit2\} \nsubseteq A_{i} Pmutex=一个无限字的集合{A0A1A2...}且满足对于所有0≤i,{crit1,crit2}⊈Ai

这就完成对系统属性的刻画，描述一下就是对于这个TS的运行轨迹来说不存在{crit1, crit2}满足条件的情况。

所以无限字可以是类似{crit1}{crit2}{crit1}{crit2}…或者∅∅∅∅∅…反正就是不能出现{crit1,crit2}这个元素。

那么再问一个问题，上面的那个TS系统满足这个PmutexP_{mutex}Pmutex性质嘛？Yes，因为从图上看不存在{crit1,crit2}的情况，所以满足了我们定义的互斥性性质。

刻画无饥饿(starvation freedom)系统的属性

不存在饥饿的系统要求满足条件:

“A process that wants to enter the critical section is eventually able to do so‘”
如果一个进程想要进入临界区，那么它最终总是能够进入临界区。

这一次让AP={crit1,wait1,crit2,wait2}

用形式化的语言描述为LT性质就是：
Pnostarve=一个无限字的集合{A0A1A2...}满足(∃∞j.waiti∈Aj)⇒(∃∞j.criti∈Aj)foreachi∈{1,2}P_{nostarve} = 一个无限字的集合\{A0A1A2...\} \\ 满足(\overset{\infty}\exist j.\;wait_{i}∈A_{j})\Rightarrow (\overset{\infty}\exist j.\;crit_{i}∈A_{j})\; for\;each\;i∈\{1,2\} Pnostarve=一个无限字的集合{A0A1A2...}满足(∃∞j.waiti∈Aj)⇒(∃∞j.criti∈Aj)foreachi∈{1,2}

其中∃∞\overset{\infty}\exist∃∞代表无限多

描述一下就是当一个进程进入等待状态后，之后肯定会进入临界区

那么基于信号量的互斥系统满足无饥饿性质嘛？no，如果是这样一条迹:∅{wait2}{wait1,wait2}{crit1,wait2}{wait2}{wait1,wait2}{crit1,wait2}...\varnothing\{wait2\}\{wait1,wait2\}\{crit1,wait2\}\{wait2\}\{wait1,wait2\}\{crit1,wait2\}...∅{wait2}{wait1,wait2}{crit1,wait2}{wait2}{wait1,wait2}{crit1,wait2}...，那么进程2将永远的不能进入临界区。

安全性(Safety Properties)和不变性(Invariants)

安全性通常被描述为“不会发生不好的事情”(nothing bad should happen)

安全性的例子

互斥性是一种典型的安全性，它要求在临界区最终只有一个进程存在，bad thing指的是在临界区存在两个或两个以上的进程，这种坏事要求永远不会发生
无死锁性(deadlock freedom)是另一个典型的安全属性。在哲学家问题中，发生死锁的特征是所有哲学家都拿起了一把筷子，并且正在等待拿起第二把筷子，这种坏的（或unwanted，即不必要的）情况要求永远都不会发生。

不变性

事实上，上述（互斥与无死锁）安全性是一种特殊的性质：不变性。不变性是LT属性，由状态的条件Φ给出，并且要求Φ对所有可达到的状态保持不变。不变性是安全性的一种，也就是安全性的子集。

如果在AP上的线性属性PinvP_{inv}Pinv是不变性，那么它具有如下形式：
Pinv={A0A1A2...∈(2AP)w∣∀j≥0.Aj⊨Φ}P_{inv}=\{A_{0}A_{1}A_{2}... ∈ (2^{AP})^{w} | ∀j \ge 0. A_{j} \vDash Φ \} Pinv={A0A1A2...∈(2AP)w∣∀j≥0.Aj⊨Φ}

其中ΦΦΦ是AP上的逻辑命题公式，ΦΦΦ被称为PinvP_{inv}Pinv的不变条件。

让我们回想一下先前的基于信号量的互斥系统，在那个系统中Φ=¬crit1∨¬crit2Φ=\lnot crit1\vee \lnot crit2Φ=¬crit1∨¬crit2,保证crit1和crit2不能同时为真。

设TS是一个没有终止状态的转换系统，那么有：
TS⊨PinvTS\vDash P_{inv}TS⊨Pinv
ifftrace(π)∈PinvforallpathsπinTSiff\; trace(\pi)∈ P_{inv}\; for\; all\; paths\;\pi \; in\; TSifftrace(π)∈PinvforallpathsπinTS
iffL(s)⊨ΦforallstatessthatbelongtoapathofTSiff\; L(s)\vDash Φ\; for\; all\; states\;s\;that\;belong\; to\; a\;path\; of\;TSiffL(s)⊨ΦforallstatessthatbelongtoapathofTS
iffL(s)⊨Φforallstatess∈Reach(TS)iff\; L(s)\vDash Φ\; for\; all\; states\;s∈Reach(TS)iffL(s)⊨Φforallstatess∈Reach(TS)

注意上面的最后一个式子，我们将TS能否满足不变性，转换成为了所有可达状态是否满足不变性这一问题。基于此我们可以设计检验不变性的算法。

我们该如何检验一个系统是否满足了不变性呢？
我们只要遍历系统的每个状态，从初始状态开始，利用深度优先(Dfs)或者广度优先(Bfs)算法，检查每一个可达状态是否满足ΦΦΦ，只要找到一个可达状态不满足ΦΦΦ，那么系统就不满足不变性，如果我们遍历所有状态发现均满足ΦΦΦ，那么系统就满足不变性。

安全性

上面我们可以看到，不变性可以被视为状态属性，并且可以通过考虑可达状态来检查。但是安全性不能仅考虑可达状态来验证，而是需要对有限路径片段提出要求。

个人理解，不变性的要求是满足所有可达状态满足要求，而安全性是要求所有的系统上出现的有限路径片段满足要求，从这个角度来看，不变性就是安全性的一种特例，如果安全性要求的有限路径片段的长度为1的话，那就变成了不变性要求。

我们考虑一个自动取款机（ATM）的例子，ATM机的要求是，只有在提供了正确的个人识别码（PIN）后，才能从自动取款机中取款。这个属性不是不变量，因为它不是一个单纯的状态属性。但是，它是一种安全性，例如
"提供正确的PIN","取款",..."提供正确的PIN","取款",..."提供正确的PIN","取款",...

这样的路径片段是满足安全性的，但如果出现
"提供错误的PIN""取款"..."提供错误的PIN""取款"..."提供错误的PIN""取款"...

这样的路径片段是是不满足安全性的，我们可以看到，一旦出现了这样"坏(bad)"的片段，不管后面如何都是不满足安全性的，我们引入前缀、坏前缀等概念来帮助我们定义安全性。

安全性定义为
对于所有的σ∈(2AP)w∖Psafe存在一个σ的有限前缀σ^满足Psafe∩{σ′∈(2AP)w∣σ^是σ′的有限前缀}=∅对于所有的\sigma∈(2^{AP})^w\setminus P_{safe}存在一个\sigma的有限前缀\hat{\sigma}满足 \\ P_{safe}\cap\{\sigma'∈(2^{AP})^w|\hat{\sigma}是\sigma'的有限前缀\}=\varnothing 对于所有的σ∈(2AP)w∖Psafe存在一个σ的有限前缀σ^满足Psafe∩{σ′∈(2AP)w∣σ^是σ′的有限前缀}=∅

解释一下，对于所有的无限字σ=A0A1A2...∈(2AP)w∖Psafe\sigma=A_{0}A_{1}A_{2}...\in(2^{AP})^w\setminus P_{safe}σ=A0A1A2...∈(2AP)w∖Psafe，存在σ\sigmaσ的有限前缀σ^=A0A1...An\hat{\sigma}=A_{0}A_{1}...A_{n}σ^=A0A1...An，使得以σ^\hat{\sigma}σ^有限前缀起始的字A0A1...AnBn+1Bn+2...A_{0}A_{1}...A_{n}B_{n+1}B_{n+2}...A0A1...AnBn+1Bn+2...不属于PsafeP_{safe}Psafe。

有限字σ^=A0A1...An\hat{\sigma}=A_{0}A_{1}...A_{n}σ^=A0A1...An被称为PsafeP_{safe}Psafe的坏前缀(bad prefix)，符号表示为BadPref(Psafe)BadPref(P_{safe})BadPref(Psafe)。

如果σ^\hat{\sigma}σ^被称为PsafeP_{safe}Psafe的最小坏前缀(minimal bad prefix)，那么就是说σ^\hat{\sigma}σ^中没有比σ^\hat{\sigma}σ^长度更小的坏前缀，符号表示为MinBadPref(Psafe)MinBadPref(P_{safe})MinBadPref(Psafe)。

对于一个TS系统满足安全性，那么当且仅当：
TS⊨PsafeTS\vDash P_{safe}TS⊨Psafe
ifftrace(TS)⊆Psafeiff\; trace(TS)\subseteq P_{safe}ifftrace(TS)⊆Psafe
ifftracefin(TS)∩BadPref=∅iff\; trace_{fin}(TS) \cap BadPref=\varnothingifftracefin(TS)∩BadPref=∅
ifftracefin(TS)∩MinBadPref=∅iff\; trace_{fin}(TS) \cap MinBadPref=\varnothingifftracefin(TS)∩MinBadPref=∅

以红绿灯系统为例，它拥有一个属性

each red phase should be immediately preceded by a yellow phase
只有在黄灯亮了之后红灯才能亮

AP定义为{red,yellow}，用形式化的符号表述为：
一个无限字的集合{A0A1A2...}对于所有i>0满足red∈Ai,yellow∈Ai−1一个无限字的集合\{A_{0}A_{1}A_{2}...\}\; 对于所有i>0满足red∈A_{i},yellow∈A_{i-1} 一个无限字的集合{A0A1A2...}对于所有i>0满足red∈Ai,yellow∈Ai−1

类似于∅∅{red}\varnothing\varnothing\{red\}∅∅{red}，∅{red}\varnothing\{red\}∅{red}都是最小坏前缀，因为red之前没有出现yellow

而类似于{yellow}{yellow}{red}{red}∅{red}\{yellow\}\{yellow\}\{red\}\{red\}\varnothing\{red\}{yellow}{yellow}{red}{red}∅{red}是坏前缀而不是最小坏前缀，因为存在比它更小的坏前缀{yellow}{yellow}{red}{red}\{yellow\}\{yellow\}\{red\}\{red\}{yellow}{yellow}{red}{red}

闭包(Closure)

迹σ∈(2AP)w\sigma∈(2^{AP})^wσ∈(2AP)w，pref(σ)pref(σ)pref(σ)代表有限前缀(finite prefixes)的集合
pref(σ)={σ^∈(2AP)∗∣σ^是σ的有限前缀}.pref(σ) = \{ \hat{σ}∈ (2^{AP})^* | \hat{σ}是σ的有限前缀\}. pref(σ)={σ^∈(2AP)∗∣σ^是σ的有限前缀}.

如果σ=A0A1...\sigma=A_{0}A_{1}...σ=A0A1...那么pref(σ)={ε,A0,A0A1,A0A1A2,...}pref(\sigma)=\{ε,A_{0},A_{0}A_{1},A_{0}A_{1}A_{2},...\}pref(σ)={ε,A0,A0A1,A0A1A2,...}

线性时间属性P的闭包定义为：
closure(P)={σ∈(2AP)w∣pref(σ)⊆pref(P)}closure(P) = \{σ∈(2^{AP})^w | pref(σ) ⊆ pref(P)\} closure(P)={σ∈(2AP)w∣pref(σ)⊆pref(P)}

LT属性P的闭包是一组无限迹的集合，其有限前缀也是P的前缀。换言之，P闭包中的无限迹没有一个前缀不是P本身的前缀。为什么要介绍这个概念呢？下文中可以看到闭包是表征安全性和活性的关键概念。

安全性和闭包：

如果P是安全属性，当且仅当closure(P)=P

活性(liveness)

安全性规定“不好的事情永远不会发生”，一个算法可以很容易地实现一个安全性，只要检验一下看看会不会出现不好的情况。但是这很多时候是不需要的，有时候没有必要保证永远不会发生不好的事情，为此需要一些其他属性来补充。这样的属性称为"活性(liveness)"属性。可以说，活性表示“好事”将来会发生(something good will happen)

活性的例子

“每个进程最终都会进入临界区”
“每个哲学家将会无限经常次吃到饭”

从上面的定义中我们就可以知道，对于活性的判断和安全性完全不同，因为安全性只要有一个坏前缀就可以驳倒安全属性，不论后面的序列如何，而活性需要考虑未来无限路径中需要满足的特性。

如果PliveP_{live}Plive是AP上上的活性，那么无论何时：
pref(Plive)=(2AP)∗pref(P_{live})=(2^{AP})^{*} pref(Plive)=(2AP)∗

PliveP_{live}Plive被称为活性，那么每个在AP上的有限字都能够扩展成为PliveP_{live}Plive中的无限字

活性 VS 安全性

活性和安全性是不相交的嘛？
是的

所有线性时间属性都是活性或者安全性嘛？
不是

有哪些既不是安全性也不是活性的例子？
例如：

机器在提供三次雪碧之后，会无限次提供啤酒

这个例子由两个部分组成，一个是“提供三次雪碧之后”，这是一个安全属性，我们给出一个坏前缀，提供一次雪碧后提供啤酒，另一部分是“无限次提供啤酒”，这是一个活性属性。所以这种包含了安全性和活性的特性，既不属于安全性也不属于活性。

是否所有的线性时间属性都可以表示为安全性和活性的交集？
是的

根据分解定理(Decomposition theorem)

对于任何AP上的线性时间属性P，存在安全性PsafeP_{safe}Psafe和活性PliveP_{live}Plive使得
P=Psafe∩PliveP=P_{safe}\cap P_{live} P=Psafe∩Plive

线性时间属性的分类（注：不变性是包含在安全性里面，中间那块黄色的区域既是安全性又是活性，代表的含义是True）

写给学生看的系统分析与验证笔记（七）——线性时间属性（Linear-Time Properties）相关推荐

写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)
目录正则安全性验证正则安全性总结之前我们将系统建模为了抽象的模型,并且刻画了相应的性质,现在终于到了模型检测最后一步--验证(verification) 如果我们将真实的系统建模为了TS,并且 ...
写给学生看的系统分析与验证笔记（十五）——计算树逻辑(Computation tree logic,CTL)
目录介绍计算树线性时间和分支时间的对比 CTL的语法 CTL的语义 CTL状态公式的语义 CTL路径公式的语义 CTL在TS上的语义 CTL等价的定义 CTL公式的性质介绍在前面我们已经介绍 ...
【系统分析与验证笔记】线性时间（Linear-Time，简称LT）
线性时间行为(Linear-Time Behavior) 路径和状态图 TSTSTS的状态图记作G(TS)G(TS)G(TS),是顶点V=SV = SV=S和边E={(s,s′∈S×S∣s′∈Post ...
《The Non-Designer's Design Book(写给大家看的设计书)》--笔记整理
The Non-Designer's Design Book(写给大家看的设计书)-笔记整理这是一本实用性书籍,阐述了设计中的四大原则:亲密性.对齐.重复和对比,并介绍了如何运用颜色.字体,以及针对 ...
【系统分析与验证笔记】Transition System模型知识点
本章目录项目到模型的转换原因本章基本词汇解释基本动作的转移公式:S→αS′S\overset{\alpha }{\rightarrow}S'S→αS′ 标签函数(Label function): ...
写给大家看的设计书阅读笔记1——设计的四大基本原则
设计的四大基本原则概述有一些基本的设计原则,每一个优秀的设计中都应用了这些原则.我们在观察评价一个设计作品时,也要从这几条基本原则去考虑. 亲密性 Proximity 彼此相关的项应当靠近,归组在一 ...
系统分析与验证课程笔记——目录
目录参考资料与引用目录前置知识知识图谱后记这个系列是研究生"系统分析与验证课程"的课程笔记记录,因为有好多篇,为了方便索引,所以写了这篇目录,也是为了能让有需要的人能够 ...
《写给大家看的设计书》《写给大家看的色彩书》《点石成金》《形式感》学习笔记...
为什么80%的码农都做不了架构师?>>> 首发:个人博客,更新&纠错&回复今天读了四本书<写给大家看的设计书><写给大家看的色彩书>& ...
《写给大家看的设计书》《写给大家看的色彩书》《点石成金》《形式感》学习笔记
首发:个人博客,更新&纠错&回复今天读了四本书<写给大家看的设计书><写给大家看的色彩书><点石成金>和<形式感>,学习学习设计. 笔 ...

写给学生看的系统分析与验证笔记（七）——线性时间属性（Linear-Time Properties）

目录