标号变迁系统（Labelled Transition System）

我不是女神ヾ 2024-04-01 12:06 58阅读 0赞

## 标号变迁系统（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 , Δ E , s 0 , E ) E=(S\_E,A\_E,\\Delta\_E,s\_\{0,E\}) E=(SE,AE,ΔE,s0,E)，其中：

*   S E ⊆ S t a t e s S\_E \\subseteq States SE⊆States 是一个有穷的状态集合，表示  E E E 的状态空间，
 *   A E ⊆ A c t A\_E \\subseteq Act AE⊆Act 是一个有穷的词汇表，表示  E E E 的行为空间，
 *   Δ E ⊆ ( S E × A E × S E ) \\Delta\_E \\subseteq (S\_E \\times A\_E \\times S\_E) ΔE⊆(SE×AE×SE) 表示  E E E 的迁移关系，
 *   s 0 , E ∈ S E s\_\{0,E\} \\in S\_E s0,E∈SE 表示  E E E 的起始状态。

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

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

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

#### 1.1 例子 ####

![在这里插入图片描述][d7e8316eedf94c60a3e2ca701dc23cdb.png]

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

对应的形式化表示为  E = ( S E , A E , Δ E , S 0 , E ) E=(S\_E,A\_E,\\Delta \_E,S\_\{0,E\}) E=(SE,AE,ΔE,S0,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\}，
 *   Δ E = \{ ⟨ 0 , g e t T o k e n , 1 ⟩ , ⟨ 1 , c a l l , 2 ⟩ , ⟨ 2 , r e p l y , 3 ⟩ , ⟨ 3 , d i s p l a y , 0 ⟩ \} \\Delta \_E=\\\{\\langle 0,getToken,1 \\rangle,\\langle 1,call,2 \\rangle,\\langle 2,reply,3 \\rangle,\\langle 3,display,0 \\rangle \\\} ΔE=\{⟨0,getToken,1⟩,⟨1,call,2⟩,⟨2,reply,3⟩,⟨3,display,0⟩\} ，
 *   S 0 , E = 0 S\_\{0,E\}=0 S0,E=0 。

### 2. LTS 的终止状态 ###

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

#### 2.1 定义 ####

LTS  E E E 中的一个状态  s s s 称为  E E 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 例子 ####

![在这里插入图片描述][c127c252b16b432cb31e2c40ffb87309.png]

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

### 3. Trace ###

#### 3.1 定义 ####

给定一个 LTS  E = ( S E , A E , Δ E , S 0 , E ) E=(S\_E,A\_E,\\Delta\_E,S\_\{0,E\}) E=(SE,AE,ΔE,S0,E) 和一个动作序列  π = l 0 , l 1 , . . . \\pi=l\_0,l\_1,... π=l0,l1,...。如果存在一个状态和动作交替的序列  s 0 , l 0 , s 1 , l 1 , . . . s\_0,l\_0,s\_1,l\_1,... s0,l0,s1,l1,... ，并且满足  ∀ i ∈ N ⋅ ( s i , l i , s i + 1 ) ∈ Δ E \\forall i \\in N \\cdot (s\_i,l\_i,s\_\{i+1\})\\in \\Delta\_E ∀i∈N⋅(si,li,si\+1)∈ΔE，那么我们称  π \\pi π 是  E E E 的一个 `trace`。

#### 3.2 例子 ####

![在这里插入图片描述][d7e8316eedf94c60a3e2ca701dc23cdb.png]

在 `图 2-1` 中， g e t T o k e n , c a l l , r e p l y , d i s p l a y , . . . getToken,call,reply,display,... getToken,call,reply,display,... 为 `图2-1` 中的 `trace` 。

### 4. Parallel Composition  ∣ ∣ || ∣∣ ###

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

#### 4.1 定义 ####

给定两个 LTS  M = ( S M , A M , Δ M , s 0 , M ) M=(S\_M,A\_M,\\Delta\_M,s\_\{0,M\}) M=(SM,AM,ΔM,s0,M) 和  E = ( S E , A E , Δ E ， s 0 , E ) E=(S\_E,A\_E,\\Delta\_E，s\_\{0,E\}) E=(SE,AE,ΔE，s0,E) ，parallel composition  ∣ ∣ || ∣∣ 是一个对称的结合操作，满足  E ∣ ∣ M E||M E∣∣M 是一个 LTS  E ∣ ∣ M = ( S E × E M , A E ∪ A M , Δ , ( s 0 , E , s 0 , M ) ) E||M=(S\_E \\times E\_\{M\},A\_E \\cup A\_M, \\Delta,(s\_\{0,E\},s\_\{0,M\})) E∣∣M=(SE×EM,AE∪AM,Δ,(s0,E,s0,M)) ，其中  Δ \\Delta Δ 是满足下面规定的最小关系集合。对于  l ∈ A E ∪ A M l \\in A\_E \\cup A\_M l∈AE∪AM，

1.  如果  l ∈ A E \\ A M l \\in A\_E \\verb|\\|A\_M l∈AE\\AM 并且  ( s , l , s ′ ) ∈ Δ E (s,l,s')\\in \\Delta\_E (s,l,s′)∈ΔE，那么  ( ( s , t ) , l , ( s ′ , t ) ) ∈ Δ ((s,t),l,(s',t))\\in \\Delta ((s,t),l,(s′,t))∈Δ ，
2.  如果  l ∈ A M \\ A E l\\in A\_M \\verb|\\|A\_E l∈AM\\AE 并且  ( t , l , t ′ ) ∈ Δ M (t,l,t')\\in \\Delta\_M (t,l,t′)∈ΔM ，那么 ( ( s , t ) , l , ( s , t ′ ) ) ∈ Δ ((s,t),l,(s,t'))\\in \\Delta ((s,t),l,(s,t′))∈Δ ，
3.  如果  l ∈ A M ∩ A E l\\in A\_M \\cap A\_E l∈AM∩AE 并且  ( s , l , s ′ ) ∈ Δ E (s,l,s')\\in \\Delta\_E (s,l,s′)∈ΔE 并且  ( t , l , t ′ ) ∈ Δ M (t,l,t')\\in \\Delta\_M (t,l,t′)∈ΔM，那么 ( ( s , t ) , l , ( s ′ , t ′ ) ) ∈ Δ ((s,t),l,(s',t'))\\in \\Delta ((s,t),l,(s′,t′))∈Δ ，

##### 4.1.1 补充集合运算符号 逆集  \\ \\verb|\\| \\ 和 补集  / \\verb|/| / #####

**补集  / \\verb|/| /**：

*  两个集中非共同元素组成的集合（也叫反交集）
 *  例 ：  \{ 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\}

**逆集  \\ \\verb|\\| \\**：

*  第二个集合减去第一个集合所包含的元素，称为逆集（也叫反差集）
 *  例 ：  \{ 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  C l i Cli Cli（ `图 2-1`）和服务器端（`图 2-3`）。服务器程序在收到客户端的服务请求调用（`call`）后，验证客户端使用的授权令牌（`verify`），然后在数据库中进行一些查询操作（`db`），最后将数据返回给客户端（`reply`）。这里我们为了简便，假设所有动作若发生，则代表了动作成功。对于 `verify` 来说，如果验证错误我们就认为该动作执行失败，程序无法进行下一步的动作。事实上，我们可以添加其他状态来代表程序的错误状态，但是这对于我们理解这些背景知识关系不大，为了简洁，所我们做了上述假设。

![在这里插入图片描述][0e6e7b41207a49b8ab6ba5ff23fb91ab.png]

其中  C l i Cli Cli 对应的形式化表示为  E = ( S E , A E , Δ E , S 0 , E ) E=(S\_E,A\_E,\\Delta \_E,S\_\{0,E\}) E=(SE,AE,ΔE,S0,E) ，其中：

其中  S e r Ser Ser 对应的形式化表示为  M = ( S M , A M , Δ M , S 0 , M ) M=(S\_M,A\_M,\\Delta \_M,S\_\{0,M\}) M=(SM,AM,ΔM,S0,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\}，
 *   Δ M = \{ ⟨ 0 , c a l l , 1 ⟩ , ⟨ 1 , v e r i f y , 2 ⟩ , ⟨ 2 , d b , 3 ⟩ , ⟨ 3 , r e p l y , 0 ⟩ \} \\Delta \_M=\\\{\\langle 0,call,1 \\rangle,\\langle 1,verify,2 \\rangle,\\langle 2,db,3 \\rangle,\\langle 3,reply,0 \\rangle \\\} ΔM=\{⟨0,call,1⟩,⟨1,verify,2⟩,⟨2,db,3⟩,⟨3,reply,0⟩\} ，
 *   S 0 , M = 0 S\_\{0,M\}=0 S0,M=0 。

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

![在这里插入图片描述][7c772595668c439484cd0d76512aeaf4.png]

*   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\}，
 *   Δ E ∣ ∣ M = \{ ⟨ 0 , g e t T o k e n , 1 ⟩ , ⟨ 1 , c a l l , 2 ⟩ , ⟨ 2 , v e r i f y , 3 ⟩ , ⟨ 3 , d b , 4 ⟩ , ⟨ 4 , r e p l y , 5 ⟩ , ⟨ 5 , d i s p l a y , 0 ⟩ \} \\Delta \_\{E||M\}=\\\{\\langle 0,getToken,1 \\rangle,\\langle 1,call,2 \\rangle,\\langle 2,verify,3 \\rangle,\\langle 3,db,4 \\rangle ,\\langle 4,reply,5 \\rangle ,\\langle 5,display,0 \\rangle \\\} Δ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 S\_\{0,E||M\}=0 S0,E∣∣M=0 。

### 5. 可达状态 ###

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

#### 5.1 定义 ####

给定一个 LTS  E = ( S E , A E , Δ , s 0 , E ) E=(S\_E,A\_E,\\Delta,s\_\{0,E\}) E=(SE,AE,Δ,s0,E) 和一个状态  s ∈ S E s\\in S\_E s∈SE 。如果存在一个状态和动作角度的序列  s 0 , l 0 , s 1 , l 1 , . . . , s n s\_0,l\_0,s\_1,l\_1,...,s\_n s0,l0,s1,l1,...,sn ，其中  n ≥ 0 n\\geq 0 n≥0 并且满足  ∀ i ∈ N ⋅ 0 ≤ j < n → ( s i , l i , s i + 1 ) ∈ Δ E \\forall i \\in N \\cdot 0 \\leq j < n \\rightarrow (s\_i,l\_i,s\_\{i+1\})\\in \\Delta \_E ∀i∈N⋅0≤j<n→(si,li,si\+1)∈ΔE ，并且有  s 0 = s 0 , E s\_0=s\_\{0,E\} s0=s0,E 和  s n = s s\_n=s sn=s，那么我们称  s s s 是（从起始状态）可达的。

[d7e8316eedf94c60a3e2ca701dc23cdb.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/0f9b63cb7a3f4fbf98e96233f673f925.png
[c127c252b16b432cb31e2c40ffb87309.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/b038b8171ecb4384ab43989e3a5bc83e.png
[0e6e7b41207a49b8ab6ba5ff23fb91ab.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/f95977e3daee47d9a60c8d7ed068630c.png
[7c772595668c439484cd0d76512aeaf4.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/61fabbaeac0f44c2b42007f59d4ac47a.png