形式化语言——时序逻辑

刺骨的言语ヽ痛彻心扉 2024-04-01 11:46 35阅读 0赞

## 时序逻辑 ##

在模型检测工具NuSMV中，时序逻辑是用来描述系统性质（或形式规约）的形式化语言，包括两类，一类是 **线性时序逻辑（Linear-time Temporal Logic, LTL）**，另一类是**分支时序逻辑（也称计算树逻辑，Computing Tree Logic，CTL）**，二者主要的区别在于采取不同的方式对 **Kripke结构** 所对应的计算树分支进行展开。

### 1. kripke structure ###

学习模型验证，有一本文献综述`Handbook of Model Checking 2018`，都是英文的，会看的很慢。里面有数学推导过程，其中有一些缩写做好笔记，比如

*  `i.e.`表示“也就是说”
 *  `such that`表示“使什么成立”
 *  `denote by`
 *  等等

`Kripke Structure` 是一种思想，和不同系统结合就会生成对应系统的结果，这也正式 `Kripke Structure` 的优秀之处。

先在CSDN中搜索大佬写的博客。

*  [一阶逻辑及其到Kripke Structure的转换][Kripke Structure]
 *  [形式化开发方法-时态逻辑][-]

博客真的少的可怜。从大佬哪里复制一些主要的，整理一下。

#### 1.1 kripke structure 定义 1 ####

`Kripke 结构` 即过渡（迁移）系统的变化，在模型检查中用来表示系统的行为，也可以用来描述上述的反应系统。

`Kripke 结构` 由状态集合（S）、过渡集合（R）以及标记函数（L）组成。该标记函数标记各状态下使得该状态为true的变量集合。

`Kripke 结构`是一个状态过渡图，路径可以建模反应系统的计算。基于此，使用一阶逻辑公式形式化并发系统。 定义 `AP` 为一组原子命题，则 `Kripke结构`  M M M 为在原子命题上的一个四元组  M = ( S , S 0 , R , L ) M = (S,S\_0,R,L) M=(S,S0,R,L)。其中

*   S S S 是有限的状态集合。
 *   S 0 S\_0 S0 是  S S S 的子集，表示初始状态。
 *   R R R 是  S S S 的笛卡儿积，表示过渡（迁移）关系，且必须包含所有的，也就是说每个  s s s 总会有  s ’ s’ s’ 使得  ( s , s ’ ) (s,s’) (s,s’) 在关系  R R R 中。
 *   L L L 是标记函数，标记原子命题使某状态为真。

### 2. 线性时序逻辑（LTL） ###

时态运算符限定于描述从一个给定状态开始的某条路径上的事件。

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

#### 2.1 特点 ####

*  将**时间**建模成**状态序列**，无限延伸到未来，该状态序列称为**计算路径**（简称“路径”），隐含了整个系统是按着一个路径向前发展演化的，隐含使用全称量词，不适用存在量词（与CTL不同）
 *  使用指示**未来**的连接词（时间操作符），只表达一条路径上的不确定性，而CTL表达多个路径

#### 2.2 构成 ####

*  项（terms）： p p p 表示原子命题
 *  经典布尔操作
    
     *   ¬ \\neg ¬（not）
     *   ∨ \\vee ∨（or）
     *   ∧ \\wedge ∧（and）
     *   → \\rightarrow →（imply, if-then）： p → q p\\rightarrow q p→q，如果  p p p 发生则会出现  q q q
 *  基本时态操作（Basic temporal operators）
    
     *   □ \\square □（G, always）
        
         *   □ p \\square p □p： p p p holds **globally** in the future.
         *  从当前时刻起， p p p 总是为真
         *  ![在这里插入图片描述][518a4f9fcd1e4687bee12192d4202905.png]
     *   ⋄ \\diamond ⋄（F, eventually）
        
         *   ⋄ p \\diamond p ⋄p： p p p holds sometime（不确定性！）in the future
         *   p p p 在以后某个时刻会真
         *  ![在这里插入图片描述][2b7c0afc32f646419b610ba49f674a3c.png]
     *   ∘ \\circ ∘（X, next）
        
         *   ∘ p \\circ p ∘p ： p p p holds next time.
         *   p p p 在下一个时刻为真
         *  ![在这里插入图片描述][c312ea22a1714d14b89d7ac597092ee4.png]
     *   ∪ \\cup ∪（strong unit）
        
         *   p ∪ q p \\cup q p∪q ：  p p p holds until  q q q holds.

#### 2.3 例子（红绿灯） ####

以红绿灯为例。

*   g r gr gr：green
 *   y e ye ye：yellow
 *   r e re re：red

性质1：信号灯按照“红、黄、绿、红、黄、绿…”的顺序变化

*  对应的LTL： □ ( ( g r ∪ y e ) ∨ ( y e ∪ r e ) ∨ ( r e ∪ g r ) ) \\square ( (gr\\cup ye) \\vee (ye \\cup re) \\vee (re \\cup gr) ) □((gr∪ye)∨(ye∪re)∨(re∪gr))

性质2：信号灯不能在同一时间出现两种以上的颜色

*  对应的LTL： □ ( ¬ ( g r ∨ y e ) ∧ ¬ ( y e ∨ r e ) ∧ ¬ ( r e ∧ g r ) ∧ ( g r ∨ y e ∨ r e ) ) \\square ( \\neg(gr \\vee ye) \\wedge \\neg (ye \\vee re) ∧ \\neg (re \\wedge gr) \\wedge (gr \\vee ye \\vee re) ) □(¬(gr∨ye)∧¬(ye∨re)∧¬(re∧gr)∧(gr∨ye∨re))

#### 2.4 流性线性时序逻辑 ####

线性时序逻辑（`Linear Temporal Logic`，`LTL`）被广泛地用来描述基于状态的性质需求。在基于事件的模型中，状态是由已经发生的事件或者行为来刻画的，而不是像传统的基于状态的模型中通过状态变量来描述。因此我们将用 `Fluent Linear Temporal Logic`（`FLTL`） 来刻画 `LTS` 的性质，即在基于事件的模型中规约基于状态的时许性质，即再基于事件的模型中规约基于状态的时序性质。

`FLTL` 其实就是把 `fluent` 作为原子命题的 LTL。

##### 2.4.1 Fluent #####

###### 2.4.1.1 Fluent 定义 ######

一个 `fluent` 是一个三元组，记作  F l = ⟨ I F l , T F l , I n i t F l ⟩ Fl=\\left \\langle I\_\{Fl\},T\_\{Fl\},Init\_\{Fl\} \\right \\rangle Fl=⟨IFl,TFl,InitFl⟩ ，其中  I F l , T F l ∈ A c t I\_\{Fl\},T\_\{Fl\} \\in Act IFl,TFl∈Act 分别表示它的发起动作集合和终止动作集合， I n i t F l Init\_\{Fl\} InitFl 代表  F l F\_l Fl 的初始真值。

###### 2.4.1.2 Fluent 解释 ######

对于一个  f l u e n t F l = ⟨ I F l , T F l , I n i t F l ⟩ fluent F\_l=\\left \\langle I\_\{Fl\},T\_\{Fl\},Init\_\{Fl\} \\right \\rangle fluentFl=⟨IFl,TFl,InitFl⟩ 来说，显然有  I F l ∩ T F l = ∅ I\_\{Fl\} \\cap T\_\{Fl\} = \\empty IFl∩TFl=∅。例如，每一个动作  l ∈ A c t l \\in Act l∈Act 可以导出一个对应的 `fluent` 记为  l ˙ = ⟨ l , A c t \\ \{ l \} , f a l s e ⟩ \\dot l = \\left \\langle l,Act \\verb|\\| \\\{l\\\},false \\right \\rangle l˙=⟨l,Act\\\{ l\},false⟩。这个表示说，当动作  l l l 发生的时候， l ˙ \\dot l l˙ 为真，发生任何其他动作的时候，这个 `fluent` 为假。

对于动作的时长，`fluent` 认为是瞬时的，也就是说当动作发生的时候，`fluent` 认为这个动作已经完成。这个主要体现在当一个动作一旦发生，就立即对 `fluent` 的真值产生影响。在下面对于 `trace` 的位置 `i` 来说，对 `fluent` 真值的影响回考虑到 `i` 位置。

##### 2.4.2  π , i ⊨ F l \\pi,i \\vDash Fl π,i⊨Fl #####

###### 2.4.2.1  π , i ⊨ F l \\pi,i \\vDash Fl π,i⊨Fl 定义 ######

一个  t r a c e π = l 0 , l 1 , . . . trace \\pi = l\_0,l\_1,... traceπ=l0,l1,... 在位置  i i i 处满足一个  f l u e n t   F l fluent \\thinspace Fl fluentFl ，记作  π , i ⊨ F l \\pi,i \\vDash Fl π,i⊨Fl，当且仅当以下的条件至少有一个成立：

* I n i t F l ∧ ( ∀ j ∈ N ⋅ 0 ≤ j ≤ i → l i ∉ T F l ) Init\_\{Fl\} \\wedge (\\forall j \\in N \\cdot 0 \\leq j \\leq i \\rightarrow l\_i \\notin T\_\{Fl\}) InitFl∧(∀j∈N⋅0≤j≤i→li∈/TFl)
 * ∃ j ∈ N ⋅ ( j ≤ i ∧ l j ∈ I F l ) ∧ ( ∀ k ∈ N ⋅ j < k ≤ i → l k ∉ T F l ) \\exist j \\in N \\cdot (j \\leq i \\wedge l\_j \\in I\_\{Fl\}) \\wedge (\\forall k \\in N \\cdot j<k \\leq i \\rightarrow l\_k \\notin T\_\{Fl\}) ∃j∈N⋅(j≤i∧lj∈IFl)∧(∀k∈N⋅j<k≤i→lk∈/TFl)

###### 2.4.2.2  π , i ⊨ F l \\pi,i \\vDash Fl π,i⊨Fl 解释 ######

*  第一个条件是说，这个 `fluent` 初始值为真，并且这个 `trace` 到位置  i i i （包括  i i i ） 为止，还没有遇到这个 `fluent` 终止动作集合中的动作，即还没有能够让这个 `fluent` 为假。
 *  第二个条件的意思是在这个 `trace` 的位置 `i` 之前（包括 `i`），已经在某个  j ≤ i j\\leq i j≤i 位置遇到了 `fluent` 的发起动作集合中的动作，但是在位置 `j` 到 `i` 之间（包括 `i`）没有遇到过任何该 `fluent` 的终止动作集合中的动作。

显然满足这两个条件中任意一个都意味着有  π , i ⊨ F l \\pi,i \\vDash Fl π,i⊨Fl。

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

在 `图2-1` 中的客户端 LTS Cli 中，我们可以定义  f l u e n t   C A L L I N G = ⟨ \{ c a l l \} , \{ d i s p l a y \} , f l a s e ⟩ fluent \\thinspace CALLING=\\left \\langle \\\{call\\\},\\\{display\\\},flase \\right \\rangle fluentCALLING=⟨\{ call\},\{ display\},flase⟩ 来表示客户端是否请求服务。对于一个  t r a c e   π 0 = g e t T o k e n , c a l l , r e p l y , d i s p l a y , . . . trace \\thinspace \\pi\_\{0\}=getToken,call,reply,display,... traceπ0=getToken,call,reply,display,... ，我们可以看到有  π 0 , 1 ⊨ C A L L I N G \\pi\_0,1 \\vDash CALLING π0,1⊨CALLING ，因为这是遇到了 `call` 动作，但是还没有遇到 `display` 动作。

类似地，我们还可以得到  π 0 , 3 ⊭ C A L L I N G \\pi\_0,3 \\nvDash CALLING π0,3⊭CALLING。

##### 2.4.3 合法的 FLTL 公式 #####

当给定了在 Act 上的所有 fluent 的集合  ϝ \\digamma ϝ ，一个 FLTL 公式可以通过标准的布尔操作符，时序操作符  X X X （next）和  U U U 进行如下的归纳定义：

*  任意的  f l u e n t   F l ∈ ϝ fluent \\thinspace F\_l \\in \\digamma fluentFl∈ϝ 是一个合法的 FLTL 公式，
 *  如果  ϕ \\phi ϕ 和  ψ \\psi ψ 是合法的 TLTL 公式，那么  ¬ ϕ \\neg \\phi ¬ϕ ， ϕ ∨ ψ \\phi \\vee \\psi ϕ∨ψ ， X ϕ X\\phi Xϕ， ϕ U ψ \\phi U \\psi ϕUψ 也都是合法的 FLTL 公式。

惯用的布尔操作符还包括：逻辑蕴含  → \\rightarrow → ，逻辑与  ∧ \\wedge ∧ 。其中  → \\rightarrow → 可以如此定义  ϕ → ψ ≡ ¬ ϕ ∨ ψ \\phi \\rightarrow \\psi \\equiv \\neg \\phi \\vee \\psi ϕ→ψ≡¬ϕ∨ψ ，而  ∧ \\wedge ∧ 可以如此定义  ϕ ∧ ψ ≡ ¬ ( ¬ ϕ ∨ ¬ ψ ) \\phi \\wedge \\psi \\equiv \\neg(\\neg \\phi \\vee \\neg \\psi) ϕ∧ψ≡¬(¬ϕ∨¬ψ) 。

##### 2.4.4  π , i ⊨ ϕ \\pi,i \\vDash \\phi π,i⊨ϕ #####

Giannakopoulou D, Magee J. Fluent model checking for event-based systems[C]//Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering. 2003: 257-266.

给定一个无穷  t r a c e   π trace \\thinspace \\pi traceπ，其是否在位置  i i i 满足公式  ϕ \\phi ϕ ，记为  π , i ⊨ ϕ \\pi,i \\vDash \\phi π,i⊨ϕ 。

* 如果 ¬ ( π , i ⊨ ϕ ) \\neg(\\pi,i \\vDash \\phi) ¬(π,i⊨ϕ)，则 π , i ⊨ ¬ ϕ \\pi,i \\vDash \\neg \\phi π,i⊨¬ϕ
 * 如果 ( π , i ⊨ ϕ ) ∨ ( π , i ⊨ ψ ) (\\pi,i \\vDash \\phi) \\vee(\\pi,i \\vDash \\psi) (π,i⊨ϕ)∨(π,i⊨ψ)，则 π , i ⊨ ϕ ∨ ψ \\pi,i \\vDash \\phi \\vee \\psi π,i⊨ϕ∨ψ
 * 如果 π , i + 1 ⊨ ϕ \\pi,i+1 \\vDash \\phi π,i\+1⊨ϕ，则 π , i ⊨ X ϕ \\pi,i \\vDash X \\phi π,i⊨Xϕ
 * 如果 ∃ j ≥ i ⋅ π , j ⊨ ψ ∧ ∀ i ≤ k < j ⋅ π , k ⊨ ϕ \\exists j \\geq i \\cdot \\pi,j \\vDash \\psi \\wedge \\forall i \\leq k < j \\cdot \\pi,k \\vDash \\phi ∃j≥i⋅π,j⊨ψ∧∀i≤k<j⋅π,k⊨ϕ，则 π , i ⊨ ϕ U ψ \\pi,i \\vDash \\phi U \\psi π,i⊨ϕUψ

由于 FLTL 是 LTL 的一个特例，所以我们同样有 LTL 中其他的时序操作符，包括  □ \\square □（always）， ⋄ \\diamond ⋄（eventually）， W W W（weak until）

##### 2.4.5  E ⊨ ϕ E \\vDash \\phi E⊨ϕ #####

###### 2.4.5.1  E ⊨ ϕ E \\vDash \\phi E⊨ϕ 定义 ######

一个  t r a c e   π trace \\thinspace \\pi traceπ 满足公式  ϕ \\phi ϕ 记为  π ⊨ ϕ \\pi \\vDash \\phi π⊨ϕ，如果有  π , 0 ⊨ ∅ \\pi,0 \\vDash \\empty π,0⊨∅。

一个 LTS  E E E 满足公式  ϕ \\phi ϕ 记为  E ⊨ ϕ E \\vDash \\phi E⊨ϕ ，如果  E E E 产生的每一条无穷序列都满足  ϕ \\phi ϕ。

###### 2.4.5.2  E ⊨ ϕ E \\vDash \\phi E⊨ϕ 例子 ######

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

总是在请求服务（`call` 动作）之后，能够把结果展示出来（`display`动作）。那么这样的一个性质可以用 FLTL 公式表示成： D I S P L A Y \_ A F T E R \_ C A L L = □ ( c a l l → ⋄ d i s p l a y ) DISPLAY\\\_AFTER\\\_CALL=\\square (call\\rightarrow \\diamond display) DISPLAY\_AFTER\_CALL=□(call→⋄display)。显然，我们可以看出来有  π 0 ⊨ D I S P L A Y \_ A F T E R \_ C A L L \\pi\_0 \\vDash DISPLAY\\\_AFTER\\\_CALL π0⊨DISPLAY\_AFTER\_CALL 以及  C l i ⊨ D I S P L A Y \_ A F T E R \_ C A L L Cli \\vDash DISPLAY\\\_AFTER\\\_CALL Cli⊨DISPLAY\_AFTER\_CALL。

### 3. 分支时序逻辑（CTL） ###

时态运算符限定于从一个给定的状态开始的**所有**可能路径上。

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

#### 3.1 构成 ####

CTL由**路径量词**和**时态算子**构成。

路径量词：

*   ∀ \\forall ∀（“for all computation paths”，全称量词，将来全部路径）
 *   ∃ \\exists ∃（“exist some computation path” ，存在量词，存在一条将来路径）

时态算子：

*   X X X（next：下一个状态）
 *   F F F（future：某个未来的状态）
 *   G G G（globally：所有的未来状态）
 *   U U U（until：路径上存在某个状态满足性质q，而且它之前的每个状态都满足性质  p p p）
 *   R R R（release：路径上从第一个状态开始，都要满足性质  q q q ，直到某个状态满足性质  p p p ）

常见表达：

*   ∀ X p \\forall X p ∀Xp：在所有未来路径上，公式在下一个状态为真
 *   ∀ F p \\forall F p ∀Fp：在所有未来路径上，公式在某个状态必然为真
    
     *  ![在这里插入图片描述][0e82a56ee832489b9f9f771c4e55450c.png]
 *   ∀ G p \\forall G p ∀Gp：在所有未来路径上，公式都永远为真
    
     *  ![在这里插入图片描述][7e54578a4970464d84fe7899d99c461e.png]
 *   ∀ ( p U q ) \\forall (p U q) ∀(pUq)：在所有未来路径都存在：公式  p p p 一直为真，直到公式  q q q 为真
 *   ∃ X p \\exists X p ∃Xp：存在一条未来路径，下一状态公式为真
 *   ∃ F p \\exists F p ∃Fp：存在一条未来路径，公式在某个状态一定为真
    
     *  ![在这里插入图片描述][a92848bf529a4d85b536c3a7e0b1c003.png]
 *   ∃ G p \\exists G p ∃Gp：存在一条未来路径，公式永为真
    
     *  ![在这里插入图片描述][76419dcf4fea493cab984c087309e799.png]
 *   E ( p U q ) E (p U q) E(pUq)：存在一条未来路径，公式  p p p 一直为真，直到公式  q q q 为真

#### 3.2 例子 ####

以进程访问共享数据为例，假设有两个进程 proc1 和 proc2，当进入“critical”状态表示正在访问共享数据，“entering”状态表示进程请求访问共享数据，当任务调度允许访问后进入“critical”状态访问共享数据。

性质1：不存在 进程1 和 进程2 同时进入“critical”状态

*  对应的CTL： ∀ G ! ( p r o c 1. s t a t e = c r i t i c a l & p r o c 2. s t a t e = c r i t i c a l ) \\forall G ! (proc1.state = critical \\& proc2.state = critical) ∀G!(proc1.state=critical&proc2.state=critical)

性质2：如果进程1处于“entering”状态（即请求进入“critical”状态），那么最终进程1都会进入“critical”状态

*  对应的CTL： ∀ G ( p r o c 1. s t a t e = e n t e r i n g → ∀ F p r o c 1. s t a t e = c r i t i c a l ) \\forall G (proc1.state = entering \\rightarrow \\forall F proc1.state = critical) ∀G(proc1.state=entering→∀Fproc1.state=critical)

### 4. 状态满足公式 ###

<table> 
 <thead> 
 <tr> 
 <th>描述</th> 
 <th>公式</th> 
 </tr> 
 </thead> 
 <tbody> 
 <tr> 
 <td>deMargan律</td> 
 <td> ¬ ( ϕ ∧ ψ ) ≡ ¬ ϕ ∨ ¬ ψ \neg (\phi \wedge \psi)\equiv \neg \phi \vee \neg \psi ¬(ϕ∧ψ)≡¬ϕ∨¬ψ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ¬ ( ϕ ∨ ψ ) ≡ ¬ ϕ ∧ ¬ ψ \neg (\phi \vee \psi)\equiv \neg \phi \wedge \neg \psi ¬(ϕ∨ψ)≡¬ϕ∧¬ψ</td> 
 </tr> 
 <tr> 
 <td>幂等律</td> 
 <td> ¬ ¬ ϕ ≡ ϕ \neg \neg \phi \equiv \phi ¬¬ϕ≡ϕ</td> 
 </tr> 
 <tr> 
 <td>对偶率</td> 
 <td> ¬ G ϕ ≡ F ¬ ϕ \neg G \phi \equiv F \neg \phi ¬Gϕ≡F¬ϕ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ¬ F ϕ ≡ G ¬ ϕ \neg F \phi \equiv G \neg \phi ¬Fϕ≡G¬ϕ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ¬ F ( ϕ U ψ ) ≡ ¬ ϕ R ¬ ψ \neg F (\phi U \psi) \equiv \neg \phi R \neg \psi ¬F(ϕUψ)≡¬ϕR¬ψ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ¬ ( ϕ R ψ ) ≡ ¬ ϕ U ¬ ψ \neg (\phi R \psi)\equiv \neg \phi U \neg \psi ¬(ϕRψ)≡¬ϕU¬ψ</td> 
 </tr> 
 <tr> 
 <td>自对偶率</td> 
 <td> ¬ X ϕ ≡ X ¬ ϕ \neg X \phi \equiv X \neg \phi ¬Xϕ≡X¬ϕ</td> 
 </tr> 
 <tr> 
 <td>分配率</td> 
 <td> F ( ϕ ∨ ψ ) ≡ F ϕ ∨ F ψ F(\phi \vee \psi) \equiv F \phi \vee F \psi F(ϕ∨ψ)≡Fϕ∨Fψ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> G ( ϕ ∨ ψ ) ≡ G ϕ ∨ G ψ G(\phi \vee \psi) \equiv G \phi \vee G \psi G(ϕ∨ψ)≡Gϕ∨Gψ</td> 
 </tr> 
 <tr> 
 <td>连接词相互定义</td> 
 <td> F ϕ ≡ ⊤ U ϕ F \phi \equiv \top U \phi Fϕ≡⊤Uϕ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> G ϕ ≡ ⊥ R ϕ G \phi \equiv \bot R \phi Gϕ≡⊥Rϕ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ϕ W ψ ≡ ϕ U ψ ∨ G ϕ \phi W \psi \equiv \phi U \psi \vee G \phi ϕWψ≡ϕUψ∨Gϕ</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ϕ W ψ ≡ R ( ϕ ∨ ψ ) \phi W \psi \equiv R(\phi \vee \psi) ϕWψ≡R(ϕ∨ψ)</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ϕ R ψ ≡ ψ W ( ϕ ∧ ψ ) \phi R \psi \equiv \psi W(\phi \wedge \psi) ϕRψ≡ψW(ϕ∧ψ)</td> 
 </tr> 
 <tr> 
 <td></td> 
 <td> ϕ U ψ ≡ ϕ W ψ ∧ F ψ \phi U \psi \equiv \phi W \psi \wedge F \psi ϕUψ≡ϕWψ∧Fψ</td> 
 </tr> 
 </tbody> 
</table>

[Kripke Structure]: https://blog.csdn.net/Solo95/article/details/82821021
[-]: https://blog.csdn.net/u013599298/article/details/52918416
[21f0ae3a793446e686cec66184b099ae.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/4f752a1b90044ca4b57fb167a568ed58.png
[518a4f9fcd1e4687bee12192d4202905.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/70780802089542fb9d485c1a360613ef.png
[2b7c0afc32f646419b610ba49f674a3c.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/e8c6c90237b04fc5b031bd2b8b062451.png
[c312ea22a1714d14b89d7ac597092ee4.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/a71cfa00b2274f28bd430a5e787e5fc1.png
[22794ef491af4d80a28518e0007affc9.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/5d8cca72fc744eeba3434c1c8a4319bc.png
[d747580a9a6946929060aa7caacc8a7d.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/3df0a44377fb4f5eb5bad77c683eb1d1.png
[326975ab46234d179e3fe6f4224b935c.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/3090953ce51442a39cab23f53090870d.png
[0e82a56ee832489b9f9f771c4e55450c.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/bd1ac675acec4f8485d2c3d945f1bdba.png
[7e54578a4970464d84fe7899d99c461e.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/996e661095574fcfa11814f74bff1d53.png
[a92848bf529a4d85b536c3a7e0b1c003.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/c0034a2353214c6e9d8c63350e45f8d2.png
[76419dcf4fea493cab984c087309e799.png]: https://image.dandelioncloud.cn/pgy_files/images/2024/04/01/0950848f7fb44735bf569244ec7f8b4d.png