计算树逻辑

线性时序逻辑LTL是基于路径的,因此是被视为线性的。在LTL中考虑从同一状态开始计算时,很容易碎全部计算同时陈述性质,但难以对部分计算陈述性质。
我们接下来介绍的计算树逻辑将基于时间的分支概念,用无限有向树来描述系统性质。这将允许我们表示开始与一个状态的某些或全部计算的性质,因而允许使用路径存在量词\(\exists\)和全称量词\(\forall\).

计算树逻辑(Computation Tree Logic, CTL)
CTL语法: 原子命题集合AP上的CTL状态公式\[\Phi := true|a|\Phi_1\land\Phi_2|\lnot \Phi|\exists\varphi|\forall\varphi\]其中\(a\in AP, \varphi\)是路径公式:\[\varphi := \bigcirc \Phi|\Phi_1\bigcup\Phi_2,\]\(\Phi\)是状态公式。

状态公式表达状态的性质,而路径公式表达状态的一个无限序列的性质。在路径公式前添加路径量词就可以转化为状态公式。可以类似LTL那样利用true和false派生出\(\Diamond,\Box\).
\(\exists\Diamond\Phi\)表示"可能成立",\(\forall\Diamond\Phi\)表示"必然成立",\(\exists\Box\Phi\)表示"可能总是,"\(\forall\Box\Phi\)表示"不变"。\(\forall\Box\forall\Diamond\Phi\)表示在所有路径上无线经常为真。
如果迁移系统TS的每个初始状态\(s_0\)满足状态公式\(\Phi\),称TS满足\(\Phi\)(\(TS\vDash\Phi\)).

LTL与CTL的表达力对比
定理1. CTL转化为等价LTL公式的准则:令\(\Phi\)是CTL公式,消去其中所有路径量词得到LTL公式\(\varphi\). 则\(\Phi\equiv\varphi\)或不存在LTL公式等价于\(\Phi\).
定理2. 存在这样的LTL公式,使不存在CTL公式与之等价。例:\(\Diamond\Box a\).
也存在这样的CTL公式,使不存在LTL公式与之等价。例:\(\forall\Box\exists\Diamond a\).

CTL模型检验
基本算法:
(1) 递归计算满足公式\(\Phi\)的所有状态的集合\(Sat(\Phi)\).
(2) \(TS\vDash\Phi\)当且仅当\(I\subseteq Sat(\Phi)\).
\(Sat(\Phi)\)的递归计算可以理解为对CTL公式自下而上的遍历,节点表示子式,叶节点为true或原子命题。所有内部节点用一个运算符标记。
叶节点的满足集可以直接由标签函数得到。

    发表于2022-02-14

正则性质

有限自动机
一个未定有限自动机(Nondeterministic Finite Automaton, NFA)是指五元组\[A=\langle Q,\Sigma, \delta,Q_0, D\rangle,\] 其中Q是有限的状态集合,\(\Sigma\)是字母表,\(\delta: Q\times \Sigma \to 2^Q\)是迁移函数,\(Q_0\)是初始状态集合,\(F\subset Q\)为接受状态集。
A接受某个有限单词w,当且仅当存在A的一个运行,使A可以将w读完,且停机在接受状态。A接受单词的集合称为A接受的语言,记作\(L(A)\).

未定有限自动机与确定有限自动机(Deterministic Finit Automation, DFA)是等价的。确定有限自动机是指\(|Q_0|\le 1\)且\(\forall q, A, |\delta(q, A)|\le 1|.\) 这一结论由迁移函数扩充到Q的幂集上可以立即得到。如果\(|Q_0|=1, |\delta(q,A)|=1,\) 称DFA是完全的。通过添加陷阱状态及其自循环可以证明DFA与完全DFA的等价性。

有限自动机的非空性与可达性是等价的,即\(L(A)\ne\emptyset \Leftrightarrow \exists q_0\in Q,q\in F\), 使得\(q\in Reach(q_0).\)

利用构造同步积等方法,可以证明有限自动机的语言(即正则语言)在交、并、补、连接和有限次重复(Kleene*)下是封闭的。

正则安全性质的模型检验
定义 正则安全性质:若\(P_{safe}\)的坏前缀集合构成字母表\(2^{AP}\)上的正则语言,称为正则安全性质。
不变式都是正则安全性质,坏前缀可由\(\Phi^*(\lnot \Phi) true^*\)刻画,这里\(\Phi\)表示所有\(A\vDash \Phi, A\in 2^{AP}\)的集合。

为了检验有限迁移系统TS是否满足正则安全性质\(P_{safe}\),只需要构造TS与A的同步积\(TS\otimes A\),其中A是检验正则安全性质的有限自动机,然后检验此迁移系统。利用A的接受状态诱导的命题逻辑公式, 可以得到一个不变式\(\Phi\), 使得\(Traces_{fin}(TS)\cap L(A) = \emptyset\)当且仅当\(TS\otimes A\vDash \Phi.\) 这样,正则安全性质的检验就转化成了不变式的检验。

设TS是无终止状态的迁移系统,\(A=\langle Q, \Sigma, \delta, Q_0, F\rangle\)是NFA,其中字母表\(\Sigma = 2^{AP}\)且\(Q_0\cap F = \emptyset\).定义乘积迁移系统如下:\[TS\otimes A = \langle S', Act, \to ', I', AP', L' \rangle\] 其中\(S' = S\times Q\), \(\rightarrow'\)由以下定义:\[\frac{s\to^a t\land q\overset{L(t)}{\to}p}{\langle s, q\rangle \to^a \langle t, p \rangle}\]\(I'=\{\langle s_0, q\rangle | s_0\in I, \exists q\in Q_0:q_0\overset{L(s_0)}{\to}q\}\),
\(AP'=Q\), \(L':S\times Q\to 2^Q\)由\(L'(\langle s, q\rangle)=\{q\}\)给出,AP'的不变式\(P_{inv(A)}\)由命题公式\[\bigwedge_{q\in F} \lnot q\]定义,简记为\(\lnot F\).

定理:TS是AP上的迁移系统,A是字母表为\(2^{AP}\)的NFA,\(P\)是AP上的正则安全性质,\(L(A)\)是其(极小)坏前缀的集合。以下命题等价:
(1) \(TS\vDash P\).
(2) \(Traces_{fin}(TS)\cap L(A)=\emptyset\).
(3) \(TS\otimes A \vDash P_{inv}(A)\).

无限单词上的自动机
\(\omega\)正则表达式:形如\[G = E_1\cdot F_1^\omega + \cdots+E_n\cdot F_n^\omega\]其中\(E_i, F_i\)为字母表\(\Sigma\)上的正则表达式,且\(\epsilon \not \in L(F_i)\). \(F^\omega\)表示无限次重复,与有限次重复\(F^*\)对应。\(\omega\)正则语言关于交、并、补是封闭的。

若AP上的LT性质P是字母表\(\Sigma = 2^{AP}\)上的正则语言,则称P是\(\omega\)正则性质。
不变式、无饥饿是\(\omega\)正则性质。无饥饿可由正则表达式\[((\{\}+\{wait\})^*\cdot (\{crit\}+\{wait, crit\}))^\omega\]描述。

未定布奇自动机(Nondeterministic Büchi Automata, NBA)是指五元组\[A=(Q, \Sigma, \delta, Q_0, F)\] 其中\(\delta: Q\times \Sigma \to 2^{Q}\)是迁移函数,\(F\subseteq Q\)是接受状态集。更多布奇自动机相关的内容可以参考布奇自动机自动机验证, 如确定布奇自动机DBA和广义未定布奇自动机GNBA。

定理1. NBA接受的语言类和\(\omega\)正则语言的类相等。
定理2. 每个GNBA都存在NBA使二者接受语言类相等。
推论3. GNBA接受的语言类与\(\omega\)正则语言的类相等。
定理4. GNBA接受的语言类在交运算下封闭。
推论5. \(\omega\)正则语言在交运算下封闭。

模型检验\(\omega\)正则性质
类似正则安全性质与NFA同步积的验证,我们利用布奇自动机来检验\(\omega\)正则性质。
设TS是无终止状态的迁移系统,A是无阻塞NBA,定义迁移系统\(TS\otimes A\):与NFA验证正则安全性质的同步积类似,不同之处在于要验证的性质由不变式\(P_{inv(A)}\)变为持久性质\(P_{pers(A)}\):"终将总是\(\lnot F\)."

定理:TS是AP上、无终止状态的有限迁移系统,A是字母表为\(2^{AP}\)的无阻塞NBA,\(P\)是AP上的\(\omega\)正则性质,\(L_\omega(A) = (2^{AP})^\omega -P\)。以下命题等价:
(1) \(TS\vDash P\).
(2) \(Traces(TS)\cap L_\omega(A)=\emptyset\).
(3) \(TS\otimes A \vDash P_{pers}(A)\).

确定好迁移系统TS后,下一个问题是如何确定\(TS\not\vDash P_{pers}\)成立。事实上,只需要检测是否存在TS的一个环路,使得环路上面有一个可达的、且违反性质的状态s。如果不存在则性质成立,否则我们将得到一个反例。

    发表于2022-02-11

线性时间性质

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

我们的验证算法将在迁移系统的状态图中进行,这里状态图是迁移系统删去动作标记后得到的有向图。记迁移系统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}.\]

    发表于2022-02-09

并发系统的建模

迁移系统(Transition System, TS)
一个迁移系统是一个六元组\[TS=(S, Act, \rightarrow, I, AP, L),\]其中
S是一个状态集合;
Act是由动作组成的集合;
\(\rightarrow \subseteq S\times Act\times S\)是迁移关系,如果\((s,a,s')\in \rightarrow\), 我们简记为\(s\overset{a}{\rightarrow}s'.\)
\(I\subseteq\)是初始状态集合;
\(AP\)是原子命题构成的集合;
\(L:S\to 2^{AP}\)是标记函数。直观上看,\(L(s)(s\in S)\)表示恰好被状态s满足的那些原子命题。
如果\(S,ACT,AP\)都有限,则称TS是有限的。

我们用Post(s)和Pre(s)表示状态s的后继和前驱。迁移系统的终止状态定义为\(Post(s)=\emptyset\)的那些状态。
用迁移系统对软硬件系统建模的关键是未定性,通过交错为独立活动的并行执行建模。交错意味着未定地选择并行进程动作的执行顺序。但是,我们也常考虑一些确定性的迁移系统.
(1) 如果\(|I|\le 1, \forall s, a ,|Post(s,a)\le 1|.\) 称此TS是动作确定的。
(2) 如果\(|I|\le 1, \forall s, A\in 2^{AP}\)都有\(Post(s) \cap \{s'|L(s')=A\}|\le 1\), 称此TS是AP确定的。

迁移系统TS的一个执行片段\(\rho\)是指有限或无限序列\[\rho = s_0 a_1 s_1 a_2 s_2\cdots.\] 无限执行片段或以终止状态结束的片段称为极大执行片段。若\(s_0\in I,\)称为起始执行片段。TS的一个执行定义为起始执行极大片段。若存在一个执行包括状态s,称s是TS可达的状态,可达状态集记作Reach(TS).

程序图
有型变量集合Var上的程序图(Program Graph, PG)是六元组\[(Loc, Act, Effect, \hookrightarrow,Loc_0, g_0),\]其中
Loc是位置的集合,
Act是动作的集合,
Effect: \(Act\times Eval(Var)\to Eval(Var)\)是效果函数,
\(\hookrightarrow\subseteq Loc\times Cond(Var)\times Act\times Loc\) 是条件迁移关系,
\(Loc_0\subseteq Loc\)是初始位置,
\(g_0\in Cond(Var)\)是初始条件。

条件迁移关系\(l\overset{g:a}{\hookrightarrow}l'\)是\((l,g,a,l')\)的简写。g称为"守卫条件"(guard),可以看做这一迁移触发的条件。当g=True时可以忽略不写。
位置\(l\in Loc\)处的行为取决于变量赋值\(\eta\). 对于\(\eta\vDash g\)的条件g,以及对应存在的条件迁移关系,l在其中做出未定选择。如果没有可行的迁移,则系统结束。
当一个迁移动作发生时,效果函数Effect调整各变量的赋值。

程序图可以解释为迁移系统,此时每个状态s视为\(\langle l,\eta\rangle\). 迁移关系将如下定义:\[\frac{l\overset{g:a}{\hookrightarrow}l'\land \eta\vDash g}{\langle l,\eta\rangle\overset{a} {\to} \langle l', Effect(a,\eta)\rangle}.\]

迁移系统的交错
设\(TS_i, TS_2\)是两个迁移系统。迁移系统\(TS_1||| TS_2\)定义为\[(S_1\times S_2, Act_1\cup Act_2, \rightarrow, I_1\times I_2, AP_1\cup AP_2, L)\]其中迁移关系包括两部分,第一部分由\[\frac{(s_1,a,s'_1)\in\rightarrow_1}{(\langle s_1,s_2\rangle, a, \langle s'_1, s_2\rangle)\in \rightarrow}\]生成,第二部分类似。而标记函数定义为\(L(\langle s_1, s_2\rangle) = L_1(s_1)\cup L_2(s_2)\).
迁移系统的交错可为异步并发建模,但不能解决共享变量等问题。

类似于迁移系统,我们可以定义程序图的交错。程序图\(PG_1|||PG_2\)的全局变量(共享变量)是\(Var_1\cap Var_2\). 在程序图的交错中,进程可以通过共享变量实现通信。
以Peterson互斥算法为例,两个进程可以通过访问或修改某个共享变量\(x\)实现通信,来确保两个进程不会同时进入关键节段中。

同步消息传递(握手)
在同步消息传递中,参与互动定的进程只能以同步的方式进行(握手). 也就是说,只有进程都同时参与互动时,进程才可以互动。
设有迁移系统\(TS_1,TS_2\)。握手动作的集合\(H\subseteq Act_1\cap Act_2\). 定义\(TS_1||_H TS_2\)的迁移关系如下:
(1) H中的动作必须同步执行, 即\[\frac{a\in H\land s_1\rightarrow^a_1 s'_1 \land s_2\rightarrow^a_2 s'_2}{(s_1,s_2)\to^a (s'_1,s'_2)}.\]
(2) 不在H中的动作按照交错定义。
Note:当\(H = Act_1\cap Act_2\)时,可以简写为\(TS_1||TS_2\); 当H为空集时,与交错\(TS_1|||TS_2\)相同。
算子\(||_H\)是可交换的。如果固定H,则算子\(||_H\)是结合的。
对于多个进程\(TS_1,TS_2,\cdots,TS_n\), 一般是两两之间通信,此时我们可以定义\(H_{ij}\subseteq Act_i\cap Act_j,\) 并且假定\(H_{ij}\cap Act_k=\emptyset.\)

通道系统
通道是一个先进先出的、可传递信息的缓冲区。通道系统广泛用于描述通信协议。
直观上,通道系统由n个进程\(P_1\sim P_n\)组成,每个\(P_i\)用通信动作扩展的程序图来描述。程序图的迁移要么是通常的条件迁移,要么是以下动作之一:
(1) \(c!v\) 沿通道c发送消息v
(2) \(c?x\) 从通道c接受消息,并将其值赋给变量x.
每个通道都有一个容量cap(c)(非负整数数或无穷)和定义域dom(c)。容量决定了缓冲区的最大数据量,当cap(c)=0时,通道相当于握手。

形式化地描述,设\(Chan\)是由通道组成的有限集合,令\[Comm = \{c!v, c?x|c\in Chan, v\in dom(c), x\in Var, dom(c)\subseteq dom(x)\}\]表示(通道)动作的集合。我们先扩展(Var, Chan)上的程序图PG的定义,与通常的流程图不同的是\[\hookrightarrow \subseteq Loc \times Cond(Var) \times (Act\cup Comm)\times Loc.\]然后,我们可以定义(Var, Chan)上的通道系统CS由\((Var_i,Chan)\)上的程序图\(PG_i\)组成,\(Var = \bigcup Var_i\), 通道系统\[CS = [PG_1 |PG_2|\cdots |PG_n].\]
迁移关系有两种,第一种是通常的条件迁移,另一种是通道条件迁移,条件guard满足时,若c非空可以执行\(c?x\),若c未满可以执行\(c!x\).

    发表于2022-02-07

自动机验证(Automatic Verification)

利用自动机验证的框架
我们即将展示的模型展示方法是基于自动机理论(automata theory)的。这允许我们将待验系统和形式化规范以相同的方法表出,即布奇自动机。
假设我们希望系统模型A满足形式规范B。于是我们只需要证明自动机接受的语言满足\[L(A)\subseteq L(B).\]这等价于\[L(A)\cap \overline{L(B)}=\emptyset.\]如果交集非空,我们就得到了A不满足B的一个反例。
事实上,验证两个自动机语言交集为空要比验证其包含关系容易得多。不过,生成一个自动机语言的补集是比较困难的。然而,如果我们采用线性时序逻辑(LTL),我们可以避免考虑补集,只需要将\(\varphi\)改为\(\lnot\varphi\)即可。

布奇自动机的结合
我们将构造性地证明布奇自动机的语言在交集和闭集运算下是封闭的。
考虑两个有共同字母表的自动机\(A_1 = \langle \Sigma, S_1, \Delta_1, I_1,L_1, F_1\rangle,\) 和\(A_2 = \langle \Sigma, S_2, \Delta_2, I_2,L_2,F_2\rangle.\)

构造\(A_1\cup A_2\)是容易的。我们不妨假定\(S_1\cap S_2 = \emptyset\),否则重新命名状态即可。定义
\[A_1 \cup A_2 = \langle \Sigma, S_1 \cup S_2, \Delta_1 \cup \Delta_2 ,I_1\cup I_2 , L_1\cup L_2, F_1 \cup F_2 \rangle,\]于是\(L(A_1\cup A_2) = L(A_1)\cup L(A_2).\) 事实上,自动机在开始时有一个非确定性的选择,既可以选择根据\(A_1\)运行,也可以选择根据\(A_2\)运行,这由对初始状态的选择决定。

下面我们考虑\(A_1\cap A_2\). 其接受的语言应当同时被\(A_1, A_2\)接受,因此当\(A_1\cap A_2\)运行时,应当模拟\(A_1, A_2\)同时运行。所以我们即将构造的状态集似乎是\(S_1\times S_2\). 但是这样的构造会给接受状态集的构造造成麻烦,我们将无法定义合适的接受状态集\(F\subseteq S_1\times S_2\).

于是我们还需要定义一种特殊的自动机:广义布奇自动机(generalized Büchi automaton).
广义布奇自动机的变化之处在于其接受状态集\(F=\{f_1,\cdots, f_m\}, f_i\subseteq S\),使得一次计算\(\rho\)被接受当且仅当 \(\forall i,inf(\rho) \cap f_i\ne \emptyset\), 换言之每个\(f_i\)都有至少一个状态在该计算序列中出现了无穷多次。

我们接下来定义广义布奇自动机\(A_1\cap A_2.\) 其状态集\(S = S_1\times S_2\), 转移函数\(\Delta \), 初始状态集\(I_1\times I_2\), 标签函数\(L\), 接受状态集\(\{F_1\times S_2, S_1\times F_2\}\).
转移函数要求同时模拟\(A_1, A_2.\) 因此\[(\langle s_1, s_2\rangle , \langle s'_1,s'_2\rangle)\in \Delta \Leftrightarrow (s_1,s'_1)\in \Delta_1\land (s_2,s'_2)\in \Delta_2.\]注意标签函数是将状态集映射为命题变量集,因此\(L(s_1, s_2)=L_1(s_1)\land L_2(s_2),\) 即两个命题的合取。如果合取后的命题可化简为false,应当删去这个状态。
注意接受状态集既要求模拟计算中的\(A_1\)经过无穷多次\(F_1\)中的某元素,也要求\(A_2\)经过无穷多次\(F_2\)中的某元素,因此这个定义是合适的。

最后,我们指出如何从广义布奇自动机转化为布奇自动机,以完成\(A_1\cap A_2\)的构造。
设广义布奇自动机的接受状态集F有m个元素(即m个S的子集),我们如下定义(平凡)布奇自动机:
状态集\(S' = \bigcup_{i=1}^m S_i,\) 这里\(S_i = S\times \{i\}.\)每个状态具有形式\((s,i),s\in S.\)
状态转移关系\(\Delta'\),\((\langle s , i\rangle ,\langle s' ,j\rangle)\in \Delta'\)当且仅当以下之一成立:
(1) \(s\in f_i,\ j=i+1\)(下标按模m理解);
(2) \(s\not\in f_i,\ j=i\).
这意味着,当且仅当s在\(f_i\)中时,i才能切换到i+1. 于是,一个计算能够无穷多次经过某一组\(f_i\times i\),当且仅当其无穷多次经过了每一组\(f_i\times i\).
由此,初始状态集\(I\times\{1\},\) 标签集\(L':L'(s,i)=L(s)\), 接受状态集\(F'=f_1\times\{1\}\)的定义是自然的。

到目前为止,我们证明了布奇自动机在交和并运算下是封闭的。除此之外,还可以证明布奇自动机在补运算下也是封闭的,在此不再赘述。

布奇自动机语言的非空性检验
如上所述,欲证明自动机A满足形式规范B,只需验证\(L(A)\cap\overline{L(B)}=\emptyset\),即只需检验某个自动机语言是否非空。我们继续做如下观察:
将自动机A的状态及其转移关系视为一个有向图。对任意一个A的计算\(\rho\),一定存在某个后缀\(\rho'\),使得\(\rho'\)的任意一个状态都在之后出现了无穷多次。(因为A的状态集是有限的,出现了有限次的状态一定在\(\rho\)中总共出现了有限次,将这一段前缀删去后即得到\(\rho'\).)
于是,\(\rho'\)中的状态形成了一个强连通分支,它们恰好就是\(inf(\rho)\)。另一方面,从初始状态出发的、可达的任一个强连通分支,也生成了自动机的一个运算。因此,检验\(L(A)\)的非空性又转化成了寻找A的可达的强连通分支。

将线性时序逻辑LTL转化成自动机
下面我们给出一种算法,将线性时序逻辑LTL的一个形式规范\(\varphi\)转化成等价的布奇自动机。
自动机的每个节点(node) s与一个公式(formula) \(\eta(s)\)相关联,满足:对任一个可接受计算\(\xi\), 如果此计算达到了状态s,设其后缀是\(\xi^i\),那么我们将得到\(\xi^i\vDash \eta(s)\).
公式\(\eta(s)\)将具有如下形式:\[(\bigwedge_{i=1...m} \nu_i)\land\bigcirc (\bigwedge_{j=1...n}\kappa_j).\]这是为了方便生成节点的后继节点。每个LTL公式可以令\(m=1,n=0\)来直接转化成此形式。
我们的想法是化简上述形式的公式。首先,我们注意到\[\mu\bigcup\psi \equiv \psi\lor(\mu\land\bigcirc \mu\bigcup\psi).\]于是我们可以将\(\mu\bigcup\psi\)指向两个子节点,都删去这个公式,其一在\(\mu_i\)中添加\(\psi\),另一个在\(\nu_i\)中添加\(\mu\),并且在\(\kappa_j\)中添加\(\mu\bigcup\psi\).
用这个方法同样可以处理\(\mu\bigvee\psi, \mu\land\psi,\mu\lor\psi,\bigcirc\mu.\) 于是,我们可以逐步消去所有的\(\bigcup,\bigvee,\land,\lor,\bigcirc.\)
现在还差\(\lnot,\Diamond,\Box\)没有解决。对于后两者,只需要注意到\(\Diamond\psi\equiv true\bigcup \psi\)和\(\Box\psi\equiv false\bigvee\psi.\) 而对于\(\lnot\),我们采用"向内递归"(inwards)将所有公式化为"规范否定形式"(negation normal form),即满足所有\(\lnot\)符号只能写在命题变量之前,如\(\lnot(\mu\lor\eta)\equiv (\lnot\mu)\land(\lnot\eta).\) 类似不难给出其余公式的递归方法。

至此我们可以化简所有的公式。用形式化的语言来描述,一个节点(node)包括以下内容:
(1) 名称(Name),节点的唯一标识。
(2) 入口(Incoming),一列指向此节点的节点。
(3) 新公式(New),旧公式(Old)和下一公式(Next). 每一部分都是一个子公式集。
每个节点代表了某些计算的后继\(\xi^k\)的时序性质(Temporal properties). 公式\(New(s)\cup Old(s)\)即以上的\(\nu_i\),其中\(Old(s)\)代表了那些已经处理过的公式。而\(Next(s)\)即以上的\(\kappa_j\).

设我们想要转化的LTL公式是\(\varphi\)。转换开始时,先构造一个初始节点,仅包括\(\varphi\)一个公式在New中,并且有唯一的入口init。init可以视为一个特殊的节点。
我们如下递归地构造节点图。
对于当前节点s(从init开始构造),检查New(s)是否有未处理的公式。
(1) 若否,则此节点的处理已完成。于是再去检查节点集中是否存在另一个节点r,使得这两个节点的Old和Next分别完全相同。此时,我们不再需要节点s,将指向s的节点转而指向r,并删去s。如果不存在这样的r,则我们将s添加到节点集中,我们获得了新的"当前节点" s',满足:
[1] s指向s'
[2] New(s')=Next(s)
[3] Old(s'), Next(s')被初始化为空集。
(2) 若是,任选New(s)中一个公式\(\eta\),将其从New中删去并移入old中,选择\(\eta\)的一个主运算符,按照以上给出的处理公式的方法,获得一至两个新节点。将New(s), Old(s), Next(s), Incoming(s)全都赋给新节点。注意,经此操作后New(s)减少。经过有限次类似操作后,New(s)将变为空集。当节点图构造完成时,所有节点的New均为空。

经过有限步操作后,公式\(\varphi\)对应的有向图构造已经完成。最后,我们再构造与\(\varphi\)等价的(广义)布奇自动机:\[B=\langle \Sigma, S, \Delta, I,L,F\rangle.\]字母表\(\Sigma\)包括AP的命题及其否定形式组成的公式;状态集S即为图中的各个节点;\(\Delta\)是图的有向边;初始状态集I是由init指向的节点组成;L(s)是Old(s)中的公式的合取;接受条件F是一些AP的子集f组成的集合族,每个元素f对应一种\(\mu\bigcup\psi\),使得f中的节点s满足:要么\(\psi\in Old(s)\),要么\(\mu\bigcup\psi\not\in Old(s).\)

模型检验的复杂性
如何度量模型检验的输入对决定模型检验的复杂性有很大影响。从时间角度来看,布奇自动机的检验可以在P时间内(甚至NL空间内)完成,但以LTL表示的模型检验是PSPACE空间的。事实上,LTL验证无论是相对于待验系统还是待验公式,都是PSPACE完全的。但从空间的角度来看,LTL形式的验证,只需要与其等价的布奇自动机指数小的空间。在实践中,我们需要相对简短、容易理解、应用广泛的验证形式。
因此,我们一般选取LTL作为验证的形式规范。

状态爆炸(State Space Explosion)问题的应对策略
如何减轻状态爆炸问题成为了模型检验的主要挑战。以下我们列举了几种可能有效的策略。
(1) 二元决策图(Binary Decision Diagrams, BDD)
二元决策图是用来表达一个布尔函数的数据结构。利用二元决策图可以避免分别地计算并存储每一个状态,而是将所有状态存储在一个不含圈的图表(DAG)中。
(2) 偏序简化(Partial Order Reduction)
偏序简化用于缩减状态空间的大小,只需要检验一部分计算即可。它充分利用了并发系统中转换的可交换性。
(3) 对称性(Symmetry)
这种方法是基于利用状态组成部分的置换(permutation). 在某些特定的置换下,一些状态之间将没有区别。因此只需要选取一些状态的代表进行检验即可。

    发表于2022-02-04

布奇自动机(Büchi automata)

\(\omega\)-自动机
设\(\Sigma\)是一个有限的字母表。定义在字母表\(\Sigma\)上的自动机\[A = (Q, \Sigma, \delta, Q_0,Acc)\]称为\(\omega\)-自动机,其中Q是一个有限的状态集合,\(\delta:Q\times \Sigma\to Q\)是一个状态转移函数,\(Q_0\)为初始状态,\(Acc\)为接受条件,形式化定义为\(Q^\omega\)的子集,这里\(Q^\omega\)表示由Q中元素构成的全体无穷序列。

\(\omega\)-自动机和有穷自动机的区别在于其关注无穷状态序列的计算,而有穷自动机研究最终停机的有限计算。但是\(\omega\)自动机并非真正运行一个无穷序列的计算,而是提供了一种将无穷计算表示为有限结构的方式,来研究它的性质。我们接下来研究的布奇自动机是一种特殊的\(\omega\)-自动机。

布奇自动机(Büchi automata)
一个布奇自动机定义为\[A = \langle \Sigma, S, \Delta, I , L ,F\rangle,\]这里\(\Sigma\)是一个有限的字母表,\(S\)是有限的状态集合,\(\Delta\subseteq S\times S\)是状态转换关系,\(I\subseteq\)是初始状态集,\(L:S\to\Sigma\)是状态上的标签集,\(F\subseteq S\)是接受状态集。注意,我们这里定义的布奇自动机是非确定性(nondeterministic)的\(\omega\)-自动机,而上面的定义是指确定性的\(\omega\)-自动机。
对于A的一次计算\(\rho\), 定义\(inf(\rho)\)为其状态序列中出现了无穷多次的状态的集合。在布奇自动机中,我们定义A接受\(\rho\)当且仅当\[\inf(\rho)\cap F\ne \emptyset.\]也就是说,运算\(\rho\)中至少有一个状态s出现了无穷多次,并且s在接受状态集F中。对于非确定性布奇自动机,如果给定一个输入,只要有一种可行的计算被接受,这个输入就被认为是可接受的。
最后,我们用\(L(A)\subseteq \Sigma^\omega\)表示布奇自动机A接受的语言。注意,这里的字母表\(\Sigma\)是在状态上贴的性质标签。

利用自动机验证的一大优势是系统的模型和它的性质用一种同样的方式表示。我们将一个系统表示为布奇自动机\(A = \langle 2^{AP}, S, \Delta, I , L ,F\rangle\), 这里AP是命题标签的幂集,\(L:S\to 2^{AP}\)是标签函数。
一般情况下,我们定义S中所有状态都是可接受状态。而在需要检验程序的公平性(fairness)时,我们会选取一些状态作为可接受状态。

确定性布奇自动机
确定性与非确定性布奇自动机并非等价的。例如,不存在一个确定性布奇自动机,使其字母表为\(\{A,\lnot A\},\)并且使得接受计算当且仅当A至多出现有限次,但可以构造一个(非确定性的)布奇自动机实现这一点。另外,确定性布奇自动机在补运算下也不封闭。

    发表于2022-02-03

线性时序逻辑(Linear Temporal Logic, LTL)

线性时序逻辑(Linear Temporal Logic, LTL)常用于形式化交错序列的性质。相比于一阶逻辑和命题逻辑,LTL更能反映状态之间的动态性质。LTL在一个静态逻辑\(U\)的基础上定义,以下我们取\(U\)为一阶和命题逻辑作为例子来定义LTL。

线性时序逻辑的语法
1. 每个\(U\)的公式(formula)也是LTL的公式。
2. 如果\(\varphi,\psi\)是LTL的公式,则以下公式也是LTL的公式:
\((\lnot \varphi),(\varphi\land\psi),(\varphi\lor\psi)\); \((\bigcirc\varphi),(\Diamond\varphi),(\Box\varphi),(\varphi\bigcup\psi),(\varphi\bigvee\psi).\)

线性时序逻辑的语义
一个LTL公式的解释(interpretation)定义在一个无穷状态序列\(\xi = x_0x_1x_2\cdots\)上。
记\(\xi ^k = x_kx_{k+1}x_{k+2}\)为从第k项开始的状态序列,则LTL公式的语义可如下定义:
(1) \(\xi^k\vDash\eta\),若\(\eta\)是静态逻辑\(U\)的公式满足\(x_k\vDash\eta\).
(2) \(\xi^k\vDash(\lnot\varphi)\),如果不成立\(\xi^k\vDash\varphi.\)
(3) \(\xi^k\vDash(\varphi\land\psi),\) 若同时成立\(\xi^k\vDash\varphi,\xi^k\vDash\psi.\)
(4) \(\xi^k\vDash(\varphi\lor\psi),\) 若至少成立一个\(\xi^k\vDash\varphi,\xi^k\vDash\psi.\)
(5) \(\xi^k\vDash(\bigcirc\varphi)\),若\(\xi^{k+1}\vDash\varphi\),称为"下次成立"(nexttime)
(6) \(\xi^k\vDash(\Diamond\varphi)\),若存在\(i\ge k,\xi^i\vDash\varphi\),称为"最终成立"(eventtually).
(7) \(\xi^k\vDash(\Box\varphi)\),若对任意\(i\ge k,\xi^i\vDash\varphi\),称为"恒成立"(always).
(8) \(\xi^k\vDash(\varphi\bigcup\psi)\),若存在\(i\ge k\),使得对\(\forall k\le j \le i-1\), 有\(\xi^j\vDash\varphi\),并且\(\xi^i\vDash \psi\), 称为\(\varphi\)成立直到(until)\(\psi\)成立.
(9) \(\xi^k\vDash(\varphi\bigvee\psi)\),若至少以下之一成立:
(i) 对每个\(i\ge k,\xi^i\vDash\psi.\)
(ii) 存在\(j\ge k,\) \(\xi^j\vDash \varphi\), 且\(\forall k\le i \le j, \xi^i\vDash \psi.\)
称为\(\varphi\) 释放(release) \(\psi\). 这意味着,\(\psi\)需要保持一直成立,直到\(\varphi\)成立(有可能不会发生),并且如果\(\varphi\)成立,则最后一步二者要同时成立。

\(\Box\Diamond\varphi\)表示在序列\(\xi\)中有无穷多个\(\xi_k\)满足\(\varphi\), 而\(\Diamond\Box\varphi\)表示序列\(\xi\)从某一项\(\xi_k\)开始恒满足\(\varphi\)。
\(\Diamond\varphi\)和\((true\bigcup\varphi)\)等价,即true一直成立,直到\(\varphi\)成立(且一定会发生);而\(\Box\varphi\)和\((false\bigvee\varphi)\)等价,即false释放\(\varphi\),但释放条件false永远不成立。
此外,我们还有\(\mu\bigvee\eta = \lnot((\lnot\mu)\bigcup(\lnot\eta)).\)

对于一个系统P,如果其每个执行的状态序列\(\xi\)都满足\(\xi\vDash\varphi\),我们称\(P\vDash\varphi\), 否则\(P\not\vDash\varphi.\)

    发表于2022-01-31

软件系统的建模简介

时序系统,并发系统和响应式系统
时序系统(Sequential System), 并发系统(Concurrent System), 响应式系统(Reactive System)是三种常见的系统模型。
时序系统是可以由输入-输出关系描述的,即连接可能的初始状态与可能的计算结果状态。因此,验证时序系统的正确性可以化规为证明一阶逻辑,即给定一个确定的初始状态条件,证明其程序必定停机,且停机状态满足给定的条件。
并发系统是利用并行计算来提高计算效率。并发系统比简单时许系统更难建模验证,因为其各个组件之间在互相传递信息。在某些特定时刻,各部分程序的运行形成了某种竞争,导致在同一时刻,整体程序可能会出现多于一种可能的执行结果。比如说,两个子程序同时试图改变某变量的结果,则其发生的不同顺序会得到不同结果。
响应式系统是指程序的各组件之间,或程序与外部环境的交互起重要作用的系统。响应式系统可以是时序系统或并发系统。验证交互式系统可能会包括对请求的响应或服务的可用性验证。

状态(States)
状态这一概念是描述一个系统的核心。它捕捉并描述了系统在执行过程中,某一特定时刻的信息。对每个状态s,其取值在程序运行过程中为true或false.
在一阶逻辑观点下,状态s可以被表示为关于程序中所有变量的一个赋值。
一个命题公式也可以描述状态,比如我们并不关心变量\(x,y\)取值情况,但我们关心在任一时刻\(x\le y\)是否成立。此时我们可以用状态\(p=true\)当且仅当\(x\le y\)来描述。
两个重要的重要集合是初始状态集(initial states)和最终状态集(final states).

状态空间(State Spaces)
一个状态空间是一个有向图\(\langle S,\Delta,I\rangle\), 这里S是由状态组成的集合,\(\Delta\subseteq S\times S\)是状态之间可行的转换关系,I是初始状态集。
我们称这样的一个图为自动机(automaton). 一个自动机的运行(run)是指一个序列\(s_0s_1\cdots\)使得\(s_o\in I,(s_i,s_{i+1})\in \Delta\), 且此序列要么无穷,要么最后一项在\(\Delta\)中没有后继。在交错模型(每个时刻,至多一个转换被执行)中,将一个系统的一次执行视为这样的一个状态序列,称为交错序列。

转换系统(Transition Systems)
转换系统展示了一个(时序或并发)系统的单位动作。一个转换系统可以用于生成一个用于描述系统的状态空间。状态空间给出了系统内不同状态的关系信息,而转换系统给出了状态空间的生成关系。因此,相对而言,转换系统更加清晰。
一个转换系统\(\langle S,T,\Theta\rangle\)定义如下:
(1) S是一个一阶结构(structure), 即包含一个标签(signature) \(G=(V,F_0,R_0)\),一个定义域D, 一个函数集F,一个关系集R,和一个映射\(f:F_0\cup R_0\to F\cup R.\) 变量集\(V\)包含了程序代码和标号所需要的字符。
(2) 一个有限的转换集\(T\), T中的每个转换t具有如下形式:\[p\ \to\ (v_1,\cdots,v_n):=(e_1,\cdots,v_n).\]这里条件p是一个没有量词的一阶逻辑公式,\(v_i\in V,e_1\)是结构G上的一阶项(term). 也就是说,在条件p成立时,\(v_i\)可以被赋值为\(e_i\),从而完成一个转换。
(3) 一个初始条件\(\Theta\),由不含量词的、变量属于\(V\)的一阶公式组成。\(\Theta\)指出了初始状态集应具备哪些条件。

对于一个转换t,其激活条件为p。如果状态s满足\(s\vDash^S p,\)称t在状态s下可激活。如果状态s经转换t变为s', 记为\(s'=t(s).\)

同时允许多个赋值似乎与转换系统中单位动作的观点相悖。然而,注意到我们将程序的标号也纳入到了变量中,因此每个转换结束后,我们可以对标号赋值以决定接下来执行哪个转换(即动作),使得每个动作是确定的。

程序的一个执行(execution)定义为:一列无穷状态\(s_0,s_1,\cdots\)满足:
(1) \(s_0\vDash^S \Theta\);
对每个\(i\ge 0\), 以下之一成立:
(2) 存在转换t,其激活条件为p,使得\(s_i\vDash^S p, s_{i+1} = t(s_i).\)
(3) 不存在满足(2)的转换t,则对\(\forall j\ge i, s_j=s_i.\)

条件(3)将有穷的(可停机的)执行序列转化成了无穷序列,从而避免了有穷于无穷的序列分类。
如果状态s出现在了任一个执行序列中,称状态s是可达的(reachable).

将命题变量分配到状态上
设AP是一个有限的命题变量集合(有时也称为单位命题(atomic propositions))。
在一个转换系统中,我们定义映射\[L_p:(S\times AP ) \to \{True,False\}.\]换言之,从每个命题的角度来看,对于每个AP中的命题p,我们选取了一部分状态满足p,其余的状态不满足;或从状态的角度来看,我们对每个状态s,都选取了一部分AP中的命题变量,称s满足这些命题,同时不满足AP中的其余命题。
这如同对每个状态贴上了一些命题的“标签”。对于有标签的转换系统,可以记作\((S,\Delta,I,L_p,2^{AP}).\)
需要指出的是,可能会有多个状态拥有完全相同的命题标签集。这说明,命题标签可能并不完全给出状态或系统的性质,只需要能给出模型检验所需信息即可。

状态空间的组合(Combining State Spaces)
如上所言,一个系统可能由多个子系统组成。我们可以在每个子系统中定义局部状态(local state), 再将各个状态空间进行组合,得到全局状态(global state)空间。
在组合子系统的状态空间之前,我们先定义双射\(L_i : T_i\to\Sigma_i\),将每个子空间的全体转换(transitions)\(T_i\)映射为一个命名。这样做的目的是,有可能来自不同子空间的多个转换拥有相同的名字,当全局执行此命名的转换时,每个子空间的这种转换都要被执行。对于那些命名唯一(不与其它子系统的转换共享命名)的转换,称为局部转换(local transition).
设每个子系统的状态空间可以表示为\(G_i = \langle S_i,\Sigma_i,\Delta_i,I_i\rangle\). 我们总是假定\(S_i\cap S_j=\emptyset,i\ne j.\) 一般地,对于的局部状态空间\(G_i,G_j\),我们用符号\(G_i\circ G_j\)来表示其组合。

异步组合(asynchronous composition)是局部状态空间组合的一种,用符号\(||\)连结。异步组合要求不同子程序的转换只能交替执行。

线性观点与分支观点
在线性观点(Linear View)下,我们关注从初始状态开始,每个交错执行的状态序列能否满足待检验的要求。设程序P的全体可行的执行集合记作EP,满足待检验条件的交错序列记作集合SP。线性观点关注是否有\(EP\subseteq SP\),但不关注任两个执行序列之间的关系(比如是否有共同的前缀)。

而在分支观点(Branching View)下,选取I中一个初始状态作为根结点,构造一棵树,每个结点是状态空间中的一个状态,其后继为可以转换到的新状态。于是此树的每条从根结点出发的最长路径对应一个可执行的状态序列。这样的树可以提供比线性观点更多的信息,如从一个给定的状态(不一定是初始状态),我们可以检验是否之后的所有状态都满足给定的条件,或者是否存在某状态满足给定的条件。分支观点能够让程序有非确定性(nondeterministic)选择时的性质更加清晰。

一般地,当系统无需与外部环境交互时(称作closed systems),采用线性观点即可;而对于需要与环境交互的系统(称作open systems),采用分支观点更合适。

偏序观点
偏序执行给出了并发系统的一种更直观的描述。交错执行的序列可以视为定义在事件中的全序集,它不区分非确定性与并发性,即可能有一些可以同时进行的转换,在交错之行序列观点下必须排序。
请注意,以上我们定义的状态空间、转换系统都是在交错序列的观点下的,即一个转换结束后才能执行下一个。
一个偏序执行(partial order execution)可以定义为\((E,\prec)\). E是由事件(events)组成的集合,\(\prec\)定义了一个偏序关系,指出\(a\prec b\)当且仅当事件b不能在a结束前开始。
偏序集的性质:传递性,反身性与反对称性。
交错执行则定义了事件集上的全序集,任意两个事件要么\(a\prec b\),要么\(b\prec a\). 但在偏序执行中,如果两个事件之间没有定义偏序关系,则它们可以同时执行。利用偏序观点可以减少定义状态之间的先后次序,从而提升建模效率。

    发表于2022-01-30