线性时序逻辑 公式_数据结构c语言版严蔚敏知识点总结[通俗易懂]

• 时态逻辑分为线性时态逻辑和分叉时态逻辑，分叉时态逻辑里面有一种逻辑叫做计算树逻辑

线性时态逻辑（Linear temporal logic，简称LTL）

线性时间属性（LT property）

• 一个线性时间属性是在AP上的一组无限路径，我们通常很难直接指出这些属性是什么，但我们可以使用逻辑简洁地指定这些属性的规律，先让我们来看一下直接指出互斥现象和饥饿自由在每个时刻的方法：
  • 在 A P = { c 1 , c 2 } AP=\{c_1,c_2\} AP={
    c1​,c2​}上指定互斥现象的方法：
    • $P_{mutex}=A_0{A}_1{A}_2\cdots$（无限字），且对于$0\le i$有 { c 1 , c 2 } ⊈ A i \{c_1,c_2\}\nsubseteq A_i {
      c1​,c2​}⊈Ai​
  • 在 A P = { c 1 , w 1 , c 2 , w 2 } AP=\{c_1,w_1,c_2,w_2\} AP={
    c1​,w1​,c2​,w2​}上指定饥饿自由的方法：
    • $P_{nostarve}=A_0{A}_1{A}_2\cdots$（无限字），且
      $(\stackrel{\infty }{\exists }j.w_1\in A_j)\Rightarrow (\stackrel{\infty }{\exists }j.c_1\in A_j)\wedge (\stackrel{\infty }{\exists }j.w_2\in A_j)\Rightarrow (\stackrel{\infty }{\exists }j.c_2\in A_j)$

• 互斥现象：两个进程不可以同时进入临界资源
• 饥饿自由：当我不停的等待进入临界资源的时候，我最终可以不停的进入临界资源

• LTL的作用：描述LT特性的逻辑，但又不给出具体的时刻，只有时间的相对特性

LTL的语法

• 命题逻辑：描述系统在某一时刻的静态行为，LTL中最常用的是以下三种：

  • 原子命题：$a\in AP$
  • 否定律：$\neg \varphi$
  • 结合律：$\varphi \wedge \psi$

• 时态算子：描述系统在轨迹下所具有的性质，最基本的有以下两种：

  • 下一时刻满足$\varphi$：$◯\varphi$，读作next
  • 每一时刻一直满足$\varphi$直到$\psi$：$\varphi \bigcup \psi$，读作until

• 由命题逻辑和时态算子派生出的算子：

  • $\varphi \vee \psi \equiv \neg (\neg \varphi \wedge \neg \psi )$
  • $\varphi \Rightarrow \psi \equiv \neg \varphi \vee \psi$
  • $\varphi \iff \psi \equiv (\varphi \Rightarrow \psi )\wedge (\psi \Rightarrow \varphi )$
  • $\varphi ⨁\psi \equiv (\varphi \wedge \neg \psi )\wedge (\neg \varphi \wedge \psi )$
  • $true\equiv \varphi \vee \psi$
  • $false\equiv \neg true$
  • $◊\varphi \equiv trueU\varphi$
    

    $◊$读作eventually，表示在未来某刻会满足$\varphi$

  • $\square \varphi \equiv \neg ◊\neg \varphi$
    

    $\square$读作always，表示在此时起开始会一直满足$\varphi$

• 这些算子是有优先级的，$\neg ,◯$优先执行，其次是$\bigcup$，然后是$\vee ,\wedge$，最后是$\to$

• 对算子的直观解释：
  

  在一条轨迹上，如果从某时刻起，每个时刻只满足$b$，即便没出现过$a$，那么该时刻也满足$a\bigcup b$

• 此时，让我们用LTL语言表达互斥现象和饥饿自由在每个时刻的逻辑：

  • 互斥现象：$\square \neg (c_1\wedge c_2)$
  • 饥饿自由：$(\square ◊w_1\Rightarrow \square ◊c_1)\wedge (\square ◊w_2\Rightarrow \square ◊c_2)$

  $\square ◊w_1$理解方法：先看最外层，把$◊w_1$看作一个$\varphi$，则$\square \varphi$表示在此时起开始会一直满足$\varphi$；再看内层$◊w_1$，表示无限经常次满足$w_1$；因此，加起来表示，在此时起开始会一直无限经常次满足$w_1$

LTL的语义

• 由LTL公式$\phi$在AP上引起的LT性质为： W o r d s ( φ ) = { σ ∈ ( 2 A P ) ω ∣ σ ⊨ φ } Words(\varphi)=\{\sigma \in (2^{AP})^\omega |\sigma \vDash \varphi \} Words(φ)={
  σ∈(2AP)ω∣σ⊨φ}，其中$\sigma$是一个轨迹，$\sigma =A_0{A}_1{A}_2\cdots$，由这个LT性质可以推出如下性质：
  • $\sigma \models true$，表示路径$\sigma$一定有一条正确的路径
  • $\sigma \models a,iffa\in A_0(i.e.,A_0\models a)$，表示当且仅当$a$是状态集合$A_0$当中的一种可能时，路径$\sigma$中包含$a$
    

    $A_0$包含了初始状态所有的可能，$a$只是其中的一种

  • $\sigma \models {\phi }_1\wedge \phi ,iff\sigma \models {\phi }_{1}and\sigma \models {\phi }_2$，表示如果路径$\sigma$中包含了状态${\phi }_1$和${\phi }_2$，那么$\sigma$包含${\phi }_1\wedge {\phi }_2$
    

    $i.e.$表示“也就是”

  • $\sigma \models \neg \phi ,iff\sigma ⊭\phi$
  • $\sigma \models ◯\phi ,iff\sigma [i..]=A_1{A}_2{A}_3\cdots \models \phi$
    

    $\sigma [i..]=A_i{A}_{i+1}{A}_{i+2}\cdots$，表示从索引$i$开始后的$\sigma$的后缀

  • $\sigma \models ◊\phi ,iff\exists j⩾0.\sigma [j..]\models \phi$
  • $\sigma \models \square \phi ,iff\forall j⩾0.\sigma [j..]\models \phi$
  • $\sigma \models \square ◊\phi ,iff\forall j⩾0.\exists ⩾\sigma [i..]\models \phi$
  • $\sigma \models ◊\square \phi ,iff\exists j⩾0.\forall ⩾\sigma [i..]\models \phi$
• 范例：
  
  根据上图，我们可以推出这个TS的四个性质：
  • 从初始状态开始，每一个状态都满足$a$，即$TS\models \square a$
  • 从初始状态开始，每一个状态都满足，如果该状态不满足$b$，则该状态满足$a\wedge \neg b$，即$TS\models \square (\neg b\Rightarrow \square (a\wedge \neg b))$
  • 从左边的初始状态$s_1$开始，下一个状态可以同时满足$a$和$b$，但从右边的初始状态开始，$s_3$的下个状态还是$s_3$，$s_3$并不能同时满足$a$和$b$，因此$TS⊭◯(a\wedge b)$
  • 从左边的初始状态$s_1$开始，每一个状态都满足$b$，直到满足$a\wedge \neg b$时，不再满足$b$，但从右边的初始状态开始，并不满足，因此$TS⊭b\bigcup (a\wedge \neg b)$

用LTL表示我们常见的性质

• 可达性（Reachability）
  • 简单的可达性（simple reachability）：$◊\psi$
  • 多条件的可达性（conditional reachability）：$\varphi \bigcup \psi$

  TS系统可以既不满足$◊a$也不满足$\neg ◊a$：
  

• 安全性（Safety）：
  • 不变性（invariant）：$\square \varphi$
• 活性（Liveness）：$\square (\varphi \Rightarrow ◊\psi )andothers$
• 公平性（Fairness）：$\square ◊\varphi andothers$
• 等价性（Equivalence）：如果$Words(\varphi )=Words(\psi )$，那么$\varphi$和$\psi$等价，表示为$\varphi \equiv \psi$
• 对偶性定律（Duality law）：
  • $\neg \square \varphi \equiv ◊\neg \varphi$
  • $\neg ◊\varphi \equiv \square \neg \varphi$
  • $\neg ◯\varphi \equiv ◯\neg \varphi$
• 对偶性定律（Idempotency law）：
  • $\square \square \varphi \equiv \square \varphi$
  • $◊◊\varphi \equiv ◊\varphi$
  • $\varphi \bigcup (\varphi \bigcup \psi )\equiv \varphi \bigcup \psi$
  • $(\varphi \bigcup \psi )\bigcup \psi \equiv \varphi \bigcup \psi$
• 吸收律（Absorption law）：
  • $◊\square ◊\varphi \equiv \square ◊\varphi$
  • $\square ◊\square \varphi \equiv ◊\square \varphi$
• 分布律（Distribution law）：
  • $◯(\varphi \bigcup \psi )\equiv (◯\varphi )\bigcup (◯\psi )$
  • $◊(\varphi \vee \psi )\equiv ◊\varphi \vee ◊\psi$
  • $\square (\varphi \wedge \psi )\equiv \square \varphi \wedge \square \psi$

  注意：

  • $◊(\varphi \bigcup \psi )\not\equiv (◊\varphi )\bigcup (◊\psi )$
  • $◊(\varphi \wedge \psi )\not\equiv ◊\varphi \wedge ◊\psi$
  • $\square (\varphi \vee \psi )\not\equiv \square \varphi \vee \square \psi$
  • 下面的这个例子说明了$◊(a\wedge b)\not\equiv ◊a\wedge ◊b$：
    
    $TS⊭◊(a\wedge b)$，但$TS\models ◊a\wedge ◊b)$

• 扩展律（Expansion laws）：
  • $\varphi \bigcup \psi \equiv \psi \vee (\varphi \wedge ◯(\varphi \bigcup \psi ))$
  • $◊\varphi \equiv \varphi \vee ◯◊\varphi ))$
  • $\square \varphi \equiv \varphi \wedge ◯\square \varphi ))$

在这篇文章里有对这几个特性的详尽介绍：【系统分析与验证笔记】 线性时态逻辑LTL和计算树逻辑CTL

公平性（Fairness）

• 定义：一条路径执行过程中所有过程均符合实际情况，则表示这个路径具有了公平性。
  • 对于不满足公平性的路径，可以将不合实际的情况过程剔除，路径便具有了公平性。
  • 无饥饿性通常是在公平性的条件下产生的。
  • 公平性通常是建立活性问题的必要手段。
• 生活实例：
  • 对于十字路口的两个红绿灯进程进程交错执行：$TS=TrLigh{t}_1||TrLigh{t}_2$，给定一个活性性质的自然语言描述为：每个红绿灯都无限经常次处于绿灯的状态。这条性质表示红绿灯在无限次状态转化的过程中，会有无限次处于绿灯的状态。
    • 轨迹： { r e d 1 , r e d 2 } , { g r e e n 1 , r e d 2 } , { r e d 1 , g r e e n 2 } , { g r e e n 1 , r e d 2 } ⋯ \{red_1,red_2\},\{green_1,red_2\},\{red_1,green_2\},\{green_1,red_2\}\cdots {
      red1​,red2​},{
      green1​,red2​},{
      red1​,green2​},{
      green1​,red2​}⋯，像这样的轨迹，满足刚才我们所说的活性，那么这条轨迹也具有安全性。
    • 轨迹： { r e d 1 , r e d 2 } , { g r e e n 1 , r e d 2 } , { r e d 1 , r e d 2 } , { g r e e n 1 , r e d 2 } ⋯ \{red_1,red_2\},\{green_1,red_2\},\{red_1,red_2\},\{green_1,red_2\}\cdots {
      red1​,red2​},{
      green1​,red2​},{
      red1​,red2​},{
      green1​,red2​}⋯，像这样的轨迹，第二个红绿灯永远为红色，不满足刚才我们所说的活性，那么这条轨迹不具有安全性。

公平性约束（Fairness constraints）

• 解释：一个程序，有一些路径永远不会执行，那么，不管这些路径执行后是正确还是错误，我们都不需要去验证它，所以我们在验证的过程中，需要加上一些约束，来避免我们去验证一些永远不会走的路径，这个约束，我们称之为公平性约束

• 基于动作的公平性用A-fair表示，有三种情况：无条件公平性、强公平性、弱公平性

  • 对于一个没有初始状态的$TS=(S,Act,\to ,I,AP,L)$

    • 无初始状态
    • $A\subseteq Act$
    • 无限执行片段$\rho =s_0\stackrel{{\alpha }_0}{\to }{s}_1\stackrel{{\alpha }_1}{\to }{s}_2\cdots$

  • 无条件公平性约束（Unconditional A-fair）：若轨迹满足无条件公平性约束，则$A$中存在的一个或多个动作可以无限经常次执行。

    • 解释：当$\rho$是一个无条件公平性路径时，对于$A$中的动作在这条路径上无限经常此执行，比如 A = { ω } ⊆ A c t { N C , W , C } , ρ = s 0 → N C s 1 → W s 2 → C s 3 → N C ⋯ s n → N C ⋯ s m → N C ⋯ A=\{ \omega \} \subseteq Act\{ NC,W,C \},\rho=s_0 \overset{NC}{\rightarrow}s_1\overset{W}{\rightarrow}s_2\overset{C}{\rightarrow}s_3\overset{NC}{\rightarrow}\cdots s_n\overset{NC}{\rightarrow}\cdots s_m \overset{NC}{\rightarrow}\cdots A={
      ω}⊆Act{
      NC,W,C},ρ=s0​→NCs1​→Ws2​→Cs3​→NC⋯sn​→NC⋯sm​→NC⋯，动作$NC$在路径上经常次执行，这个路径就叫做无条件公平路径
    • 公式：
      $$true\Rightarrow \forall k⩾0,\exists j⩾k,{\alpha }_j\in A$$
      对轨迹中的动作序列的任一位置$k$，总能在$k$上或$k$后面找到一个位置$j$，该位置的动作${\alpha }_j\in A$

  • 强公平性（Strongly A-fair）：若轨迹满足强公平性约束，如果$A$中存在的动作无限经常次想要执行，则会导致$A$中存在一个或多个动作可以无限经常次执行。

    • 公式：
      $$(\forall k⩾0,\exists j⩾k,Act(s_j)\cap A\ne \varnothing )\Rightarrow \forall k⩾0,\exists j⩾k,{\alpha }_j\in A$$
      对轨迹中的状态序列的任一位置$k$，若总能在$k$上或$k$后面找到一个位置$j$，使得状态$s_j$的所有直接动作$Act(s_j)$中存在$A$中的动作（即$Act(s_j)\cap A\ne \varnothing$，无限经常次想要执行），那么$A$中一定存在无限经常次执行的动作

  • 弱公平性（Weakly A-fair）：若轨迹满足弱公平性约束，如果$A$中的某时刻开始，无限经常次有$A$中的动作想要执行，则会导致$A$中存在一个或多个动作可以无限经常次执行。

    • 公式：
      $$(\exists k⩾0,\forall j⩾k,Act(s_j)\cap A\ne \varnothing )\Rightarrow \forall k⩾0,\exists j⩾k,{\alpha }_j\in A$$
      对轨迹中的状态序列的某一位置$k$，若总能在$k$上或$k$后面找到一个位置$j$，使得状态$s_j$的所有直接动作$Act(s_j)$中存在$A$中的动作（即$Act(s_j)\cap A\ne \varnothing$，无限经常次想要执行），那么$A$中一定存在无限经常次执行的动作

    其中， A c t ( s ) = { α ∈ A c t ∣ ∃ s ′ ∈ S , s → α s ′ } Act(s) = \{ \alpha \in Act | \exist s’ \in S,s\overset{\alpha}{\rightarrow} s’ \} Act(s)={
    α∈Act∣∃s′∈S,s→αs′}

  • 例题一：

    • 取动作 A = { e n t e r 1 , e n t e r 2 } A=\{enter_1,enter_2 \} A={
      enter1​,enter2​}，判断下面的红色轨迹是否满足强公平性？（红色轨迹从第2个位置开始，234位置的状态轮以闭圈的形式无限次执行）
      
    • 答案：
      • 在红色轨迹中，我们看到，状态$⟨w_1,n_2,y=1⟩$无限次想要执行$ente{r}_1$，状态$⟨w_1,w_2,y=1⟩$无限次想要执行$ente{r}_1$和$ente{r}_2$，轨迹最终的结果是无限经常次执行$ente{r}_2$，所以这个轨迹满足强公平性。

  • 例题二：

    • 取动作 A = { r e q 2 } A=\{req_2 \} A={
      req2​}，判断下面的红色轨迹是否满足弱公平性？（红色轨迹从第1个位置开始，123位置的状态轮以闭圈的形式无限次执行）
      

    • 答案：

      • 在红色轨迹中，我们看到，从第一个状态开始，每一个状态都无限经常次想要执行$re{q}_2$，但$A$中不存在无限经常次执行的动作，所以这个轨迹不满足弱公平性。

• 程序或进程在无条件公平性下终止的情况：
  $$\begin{array}{rl}procInc=& while⟨x⩾0dox:=x+1⟩od\\ procReset=& x:=-1\end{array}$$

  $x$是共享变量，初始值为0

• 公平性对路径的约束过强或过弱

  • 公平性的目的是排除“不合理”的路径，但如果我们去除了过度或者取出不足时，对验证结果会产生一定的影响。
  • 约束过强（去除过度时）：
    • 总的路径$\subseteq$合理的路径$\subseteq$验证用的路径
    • 如果验证结果为false，则可以说明合理的路径对应的模型是有问题的
    • 如果验证的结果为true，无法说明合理的路径对应的模型是正确的
  • 约束过弱（去除不足时）：
    • 总的路径$\subseteq$验证用的路径$\subseteq$合理的路径
    • 如果验证结果为true，则可以说明合理的路径对应的模型是正确的
    • 如果验证的结果为false，无法说明合理的路径对应的模型是错误的

关于公平性的这部分，我在另一篇文章里进行了讲解，但为了方便理解关于LTL的公平性约束问题，我有将这部分内容重新粘贴了过来，另一篇文章的链接为：【系统分析与验证笔记】 线性时态逻辑LTL和计算树逻辑CTL

LTL的公平性约束

假设$\varphi$和$\psi$是在AP上的命题逻辑公式，则

• 无条件的LTL公平性约束的形式如下：$ufair=\square ◊\psi$
• 强LTL公平性约束的形式如下：$sfair=\square ◊\varphi \to \square ◊\psi$，从此刻起每时每刻都会想要在未来某时刻想要执行$\varphi$，则从此刻起每时每刻都会能够在未来某时刻能够执行$\psi$
• 弱LTL公平性约束的形式如下：$wfair=◊\square \varphi \to ◊\square \psi$，在未来某一时刻起会一直想要执行$\varphi$，则在在未来某一时刻会一直能够执行$\psi$

$\varphi$表示想要执行，$\psi$表示能够执行

LTL的公平性假设

• 强公平性假设：$sfair=\bigcup _{0<i⩽k}(\square ◊{\varphi }_i\to \square ◊{\psi }_i)$
• 通用格式：$fair=ufair\wedge sfair\wedge wfair$
• 经验法则：强或无条件公平性假设有利于解决争议，弱的公平性足以解决由交织产生的不决定性

计算树逻辑（ Computation tree logic，简称CTL）

线性时态逻辑和分支时态逻辑

• 线性时态逻辑：以状态开始的（所有）路径的语句。例如:
  • $s\models \square (x⩽20)$，表示从s开始的所有路径都满足$x⩽20$
• 分支时态逻辑：关于以一个状态开始的所有或某些路径的语句。例如:
  • $s\models \forall \square (x⩽20)$，表示从s开始的所有路径都满足$x⩽20$
  • $s\models \exists \square (x⩽20)$，表示从s开始存在路径满足$x⩽20$

检查LTL中是否有$\exists \phi$，可以用CTL的$\forall \neg \phi$检测

转移系统（Transition systems）到树（Trees）的转换

Transition systems：

Trees：

我们看到，这个Transition systems有着无穷无尽的路径，我们用数来表示各个路径，但没有办法将其全部表示出来，图中表示了前四次转移，虽然没有办法全部表示，但我们可以根据Transition systems来判断某条路径是否满足某性质。

状态和算子

• 状态上的语句：
  • 原子命题：$a\in AP$
  • 否定律：$\neg \varphi$
  • 结合律：$\varphi \wedge \psi$
  • 存在一条实现$\varphi$的路径：$\exists \varphi$
  • 所有路径都可以实现$\varphi$：$\forall \varphi$
• 路径上的语句：
  • 下一个状态满足：$◯\varphi$
  • $\varphi$一直满足直到$\psi$满足：$\varphi \bigcup \psi$

  $◯$和$\bigcup$会与$\exists$和$\forall$交替使用

• 派生算子：
  • 存在路径满足$\varphi$：$\exists ◊\varphi \equiv \exists (true\bigcup \varphi )$
  • 所有路径满足$\varphi$：$\forall ◊\varphi \equiv \forall (true\bigcup \varphi )$
  • 存在路径总是满足$\varphi$：$\exists \square \varphi \equiv \neg \forall ◊\neg \varphi$
  • 所有路径总是满足$\varphi$：$\forall \square \varphi \equiv \neg \exists ◊\neg \varphi$
  • 弱直到：
    $\exists (\varphi W\psi )\equiv \neg \forall ((\varphi \wedge \neg \psi )\bigcup (\neg \varphi \wedge \neg \psi ))$
    $\forall (\varphi W\psi )\equiv \neg \exists ((\varphi \wedge \neg \psi )\bigcup (\neg \varphi \wedge \neg \psi ))$

语义

语义学的可视化化

CTL状态公式的语义学

$s\models \varphi$表示当且仅当公式$\varphi$在状态$s$中成立

• $s\models a$，在$a$属于从状态$s$出发的路径中的一条路径时，时成立，即$a\in L(s)$
• $s\models \neg \varphi$，$iff\neg (s\models \varphi )$
• $s\models \neg \varphi$，$iff(s\models \varphi )(s\models \psi )$
• $s\models \exists \varphi$，$iff$从$s$开始的一些路径$\pi$满足$\pi \models \varphi$
• $s\models \forall \varphi$，$iff$从$s$开始的所有路径$\pi$满足$\pi \models \varphi$

CTL路径公式的语义学

$\pi \models \varphi$表示路径$\pi$满足公式$\varphi$

• $\pi \models ◯\varphi iff\pi [1]\models \varphi$
• $\pi \models \varphi \bigcup \psi iff(\exists j⩾0.\pi [j]\models \psi \wedge \forall 0⩽k<j.\pi [k]\models \varphi )$

$\pi [i]$表示在路径$\pi$上面的状态$s_i$

迁移系统语义

• 满足CTL状态公式$\varphi$的集合$Sat(\varphi )$定义为： S a t ( ϕ ) = { s ∈ S ∣ s ⊨ ϕ } Sat(\phi) =\{s \in S | s \vDash \phi \} Sat(ϕ)={
  s∈S∣s⊨ϕ}
• 当所有初始状态满足$\varphi$时，TS满足CTL公式：$TS\models \varphi iff{\forall }_{s_0}\models \varphi$

TS可能不满足$\varphi$也不满足$\neg \varphi$，即$TS⊭\varphi andTS⊭\neg \varphi$

CTL的一些常用性质

• 等价性（equivalence）：如果两个CTL:$\varphi$和$\psi$的$Sat(\varphi )=Sat(\psi )$，则$\varphi$和$\psi$等价，即$\varphi \equiv \psi$
  $$\varphi \equiv \psi iffTS\models \varphi \wedge TS\models \psi$$

• 扩展律（Expansion laws）

  • $\forall (\varphi \bigcup \psi )\equiv \psi \vee (\varphi \wedge \forall ◯\forall (\varphi \bigcup \psi ))$
  • $\forall ◊\varphi \equiv \varphi \vee \forall ◯\forall ◊\varphi$
  • $\forall \square \varphi \equiv \varphi \wedge \forall ◯\forall \square \varphi$
  • $\exists (\varphi \bigcup \psi )\equiv \psi \vee (\varphi \wedge \forall ◯\forall (\varphi \bigcup \psi ))$
  • $\exists ◊\varphi \equiv \varphi \vee \exists ◯\exists ◊\varphi$
  • $\exists \square \varphi \equiv \varphi \wedge \exists ◯\exists \square \varphi$

• 分布律（Distributive laws）

  • $\forall \square (\varphi \wedge \psi )\equiv \forall \square \varphi \wedge \forall \square \psi$
  • $\exists ◊(\varphi \vee \psi )\equiv \exists ◊\varphi \vee \exists ◊\psi$

  • $\exists \square (\varphi \wedge \psi )\not\equiv \exists \square \varphi \wedge \exists \square \psi$
  • $\forall ◊(\varphi \vee \psi )\equiv \forall ◊\varphi \vee \forall ◊\psi$

今天的文章线性时序逻辑 公式_数据结构c语言版严蔚敏知识点总结[通俗易懂]分享到此就结束了，感谢您的阅读。