标号变迁系统（Labelled Transition System）

标号变迁系统（Labelled Transition System）

在计算机科学中，迁移系统（Transition System）常被用来建模一个系统。非正式的来讲，迁移系统可看成是一个有向图。它的结点表示状态，有向边表示状态的变化。常见的迁移系统包括两种：

• 一种关注结点即状态，用状态来描述系统在某一时刻的性质，标记的是结点上的属性。
• 另一种迁移系统关注的是有向边，也即迁移行为，标注的是动作事件。

第二种迁移系统，称为标号变迁系统（Labelled Transition System），简称为 LTS，是一种特殊迁移系统，它主要关注的是系统的行为（或称为事件）。LTS 的名字来源于，它的迁移（transition）都由一个动作事件（action／event）来标记，它关注的是这些**标记（label）而非具体的状态（state）**本身。LTS 中所有行为的集合称为它的词汇表。

因此，LTS 常用在基于行为的形式化建模中。注意：基于状态的迁移系统和基于事件的迁移系统是可互相表示的（等价的）。

1. 标号迁移系统 LTS 的定义

我们使用 States 表示所有可能的状态的集合，Act 表示所有的行为标签的集合。一个 LTS 是一个四元组 $E=(S_E,A_E,{\Delta }_E,s_{0,E})$，其中：

• $S_E\subseteq States$ 是一个有穷的状态集合，表示 $E$ 的状态空间，
• $A_E\subseteq Act$ 是一个有穷的词汇表，表示 $E$ 的行为空间，
• ${\Delta }_E\subseteq (S_E\times A_E\times S_E)$ 表示 $E$ 的迁移关系，
• $s_{0,E}\in S_E$ 表示 $E$ 的起始状态。

通常为了更加直观地反映迁移动作，对于 LTS $E$ 的两个状态 $s$ 和 $t$ ，我们用符号 $s\stackrel{a}{\to }t$ 来表示 $(s,a,t)\in {\Delta }_E$ 。

正如前文所说，迁移系统可以看成一个有向图，所当迁移系统规模较小的时候，我们可以用有向图来更直观地展示一个迁移系统。

有的时候，为了使迁移边的指向方向一致，会规定除了指示起始结点的边以外的所有的边的指向方向，比如与顺时针方向一致。

1.1 例子

图2-1 表示了一个简单系统的 LTS 模型。其中用一个没有源结点的箭头来指向起始状态。这个系统首先请求一个授权令牌（getToken 动作），然后使用这个授权令牌来调用某些外部服务（call 动作）。在得到回复（reply 动作）之后，将结果显不给用户（display 动作）。

对应的形式化表示为 $E=(S_E,A_E,{\Delta }_E,S_{0,E})$ ，其中：

• S E = { 0 , 1 , 2 , 3 } S_E=\{0,1,2,3\} SE​={0,1,2,3}，
• A E = { g e t T o k e n , c a l l , r e p l y , d i s p l a y } A_E=\{getToken,call,reply,display\} AE​={getToken,call,reply,display}，
• ${\Delta }_E=\{⟨0,getToken,1⟩,⟨1,call,2⟩,⟨2,reply,3⟩,⟨3,display,0⟩\}$ ，
• $S_{0,E}=0$ 。

2. LTS 的终止状态

LTS 的终止状态（terminal state）直观上就是那些不能迁移到其他状态的状态。在有向图的表示中，就是没有指向其他结点的出边的那些结点。形式化的定义如下：

2.1 定义

LTS $E$ 中的一个状态 $s$ 称为 $E$ 的终止状态，当且仅当有 { t ∣ ∃ a ∈ A E ⋅ ( s , a , t ) ∈ Δ E } = ∅ \{t|\exists a\in A_E \cdot (s,a,t)\in \Delta_E\}=\empty {t∣∃a∈AE​⋅(s,a,t)∈ΔE​}=∅ 。

2.2 例子

例如 图2-2 所示，状态 4 为终止状态，这个 LTS 的行为相当于 图2-1 中的一次性执行然后就终止。

3. Trace

3.1 定义

给定一个 LTS $E=(S_E,A_E,{\Delta }_E,S_{0,E})$ 和一个动作序列 $\pi =l_0,l_1,...$。如果存在一个状态和动作交替的序列 $s_0,l_0,s_1,l_1,...$ ，并且满足 $\forall i\in N\cdot (s_i,l_i,s_{i+1})\in {\Delta }_E$，那么我们称 $\pi$ 是 $E$ 的一个 trace。

3.2 例子

在 图 2-1 中，$getToken,call,reply,display,...$ 为 图2-1 中的 trace 。

4. Parallel Composition $||$

在现实生活中，很多硬件或者软件系统都是并行的，所接下来我们看一下，如果利用 LTS 来建模并行系统。

4.1 定义

给定两个 LTS $M=(S_M,A_M,{\Delta }_M,s_{0,M})$ 和 $E=(S_E,A_E,{\Delta }_E，s_{0,E})$ ，parallel composition $||$ 是一个对称的结合操作，满足 $E||M$ 是一个 LTS $E||M=(S_E\times E_M,A_E\cup A_M,\Delta ,(s_{0,E},s_{0,M}))$ ，其中 $\Delta$ 是满足下面规定的最小关系集合。对于 $l\in A_E\cup A_M$，

1. 如果 $l\in A_E\text{}{A}_M$ 并且 $(s,l,s^{\prime })\in {\Delta }_E$，那么 $((s,t),l,(s^{\prime },t))\in \Delta$ ，
2. 如果 $l\in A_M\text{}{A}_E$ 并且 $(t,l,t^{\prime })\in {\Delta }_M$ ，那么$((s,t),l,(s,t^{\prime }))\in \Delta$ ，
3. 如果 $l\in A_M\cap A_E$ 并且 $(s,l,s^{\prime })\in {\Delta }_E$ 并且 $(t,l,t^{\prime })\in {\Delta }_M$，那么$((s,t),l,(s^{\prime },t^{\prime }))\in \Delta$ ，

4.1.1 补充集合运算符号 逆集 $\text{}$ 和 补集 $\text{/}$

补集 $\text{/}$：

• 两个集中非共同元素组成的集合（也叫反交集）
• 例 ： { 1 , 2 , 3 } / { 1 , 3 , 4 } = { 2 , 4 } \{1,2,3\} \verb|/| \{1,3,4\}=\{2,4\} {1,2,3}/{1,3,4}={2,4}

逆集 $\text{}$：

• 第二个集合减去第一个集合所包含的元素，称为逆集（也叫反差集）
• 例 ： { 1 , 2 , 3 } \ { 1 , 3 , 4 } = { 4 } \{1,2,3\} \verb|\| \{1,3,4\}=\{4\} {1,2,3}\{1,3,4}={4}

4.2 例子

考虑一个并行的系统，它有两部分组成，客户端 LTS $Cli$（ 图 2-1）和服务器端（图 2-3）。服务器程序在收到客户端的服务请求调用（call）后，验证客户端使用的授权令牌（verify），然后在数据库中进行一些查询操作（db），最后将数据返回给客户端（reply）。这里我们为了简便，假设所有动作若发生，则代表了动作成功。对于 verify 来说，如果验证错误我们就认为该动作执行失败，程序无法进行下一步的动作。事实上，我们可以添加其他状态来代表程序的错误状态，但是这对于我们理解这些背景知识关系不大，为了简洁，所我们做了上述假设。

其中 $Cli$ 对应的形式化表示为 $E=(S_E,A_E,{\Delta }_E,S_{0,E})$ ，其中：

• S E = { 0 , 1 , 2 , 3 } S_E=\{0,1,2,3\} SE​={0,1,2,3}，
• A E = { g e t T o k e n , c a l l , r e p l y , d i s p l a y } A_E=\{getToken,call,reply,display\} AE​={getToken,call,reply,display}，
• ${\Delta }_E=\{⟨0,getToken,1⟩,⟨1,call,2⟩,⟨2,reply,3⟩,⟨3,display,0⟩\}$ ，
• $S_{0,E}=0$ 。

其中 $Ser$ 对应的形式化表示为 $M=(S_M,A_M,{\Delta }_M,S_{0,M})$ ，其中：

• S M = { 0 , 1 , 2 , 3 } S_M=\{0,1,2,3\} SM​={0,1,2,3}，
• A M = { c a l l , v e r i f y , d b , r e p l y } A_M=\{call,verify,db,reply\} AM​={call,verify,db,reply}，
• ${\Delta }_M=\{⟨0,call,1⟩,⟨1,verify,2⟩,⟨2,db,3⟩,⟨3,reply,0⟩\}$ ，
• $S_{0,M}=0$ 。

我们把它们中相同名宇的动作看成需要同步的共享动作。如果有相同的名字但是不想成为共享动作，我们在进行 Parallel Composition 操作前可重命名该动作的名字或者隐藏该动作使得其对 Parallel Composition 不可见。因此在默认情况下，本论文将把所有 Parallel Composition 中的 LTS 之间的相同名字的动作认为需要同步执行的。客户端和服务端的 Parallel Composition 的结果 $Cli||Ser$ 如 图 2-4 所示。

• S E ∣ ∣ M = { 0 , 1 , 2 , 3 , 4 , 5 } S_{E||M}=\{0,1,2,3,4,5\} SE∣∣M​={0,1,2,3,4,5}，
• A E ∣ ∣ M = { g e t T o k e n , c a l l , v e r i f y , d b , r e p l y , d i s p l a y } A_{E||M}=\{getToken,call,verify,db,reply,display\} AE∣∣M​={getToken,call,verify,db,reply,display}，
• ${\Delta }_{E||M}=\{⟨0,getToken,1⟩,⟨1,call,2⟩,⟨2,verify,3⟩,⟨3,db,4⟩,⟨4,reply,5⟩,⟨5,display,0⟩\}$ ，
• $S_{0,E||M}=0$ 。

5. 可达状态

一个系统中可能会有一些永远不会执行的功能，例如代码中的永远都为假的条件分支。那么在建模得到的 LTS 中，就可能会有一些不可达状态，即从该 LTS 的起始状态没有一个 trace 前缀可达到该状态。形式化的定义如下。

5.1 定义

给定一个 LTS $E=(S_E,A_E,\Delta ,s_{0,E})$ 和一个状态 $s\in S_E$ 。如果存在一个状态和动作角度的序列 $s_0,l_0,s_1,l_1,...,s_n$ ，其中 $n\ge 0$ 并且满足 $\forall i\in N\cdot 0\le j<n\to (s_i,l_i,s_{i+1})\in {\Delta }_E$ ，并且有 $s_0=s_{0,E}$ 和 $s_n=s$，那么我们称 $s$ 是（从起始状态）可达的。