本文已参与「新人创造礼」活动，一起敞开创造之路。

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

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

线性时间特点（LT property）

一个线性时间特点是在AP上的一组无限途径，咱们通常很难直接指出这些特点是什么，但咱们能够运用逻辑简洁地指定这些特点的规律，先让咱们来看一下直接指出互斥现象和饥饿自在在每个时间的方法：
- 在 $AP=\{c_1,c_2\}$ 上指定互斥现象的方法：
  - $Pmutex=A0A1A2⋯P_{mutex}=A_0A_1A_2\cdots$ （无限字），且关于 $0≤i0\leq i$ 有 ${c1,c2}⊈Ai\{c_1,c_2\}\nsubseteq A_i$
- 在 $AP=\{c_1,w_1,c_2,w_2\}$ 上指定饥饿自在的方法：
  - $Pnostarve=A0A1A2⋯P_{nostarve}=A_0A_1A_2\cdots$ （无限字），且 $(∃∞j.w1∈Aj)⇒(∃∞j.c1∈Aj)∧(∃∞j.w2∈Aj)⇒(∃∞j.c2∈Aj)(\overset{\infty}{\exists } j.w_1 \in A_j)\Rightarrow (\overset{\infty}{\exists } j.c_1 \in A_j)\wedge (\overset{\infty}{\exists } j.w_2 \in A_j)\Rightarrow(\overset{\infty}{\exists } j.c_2 \in A_j)$

互斥现象：两个进程不能够一起进入临界资源

饥饿自在：当我不停的等候进入临界资源的时分，我终究能够不停的进入临界资源

LTL的作用：描绘LT特性的逻辑，但又不给出详细的时间，只要时间的相对特性

LTL的语法

出题逻辑：描绘体系在某一时间的静态行为，LTL中最常用的是以下三种：
- 原子出题： $\in AP$
- 否规律： $\neg \phi$
- 结合律： $∧\phi \wedge \psi$
时态算子：描绘体系在轨道下所具有的性质，最基本的有以下两种：
- 下一时间满意 $\phi$ ： $◯\bigcirc \phi$ ，读作next
- 每一时间一向满意 $\phi$ 直到 $\psi$ ： $⋃\phi \bigcup \psi$ ，读作until
由出题逻辑和时态算子派生出的算子：
- $∨≡(∧)\phi \vee \psi \equiv \neg(\neg \phi \wedge \neg \psi)$
- $⇒≡∨\phi \Rightarrow \psi \equiv \neg \phi \vee \psi$
- $⇔≡(⇒)∧(⇒)\phi \Leftrightarrow \psi \equiv (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi)$
- $⨁≡(∧)∧(∧)\phi \bigoplus \psi \equiv (\phi \wedge \neg \psi) \wedge (\neg \phi \wedge \psi)$
- $\equiv \phi \vee \psi$
- $\equiv \neg true$
- $◊≡trueU\Diamond \phi \equiv true \ U \phi$
  
  $◊\Diamond$ 读作eventually，表明在未来某刻会满意 $\phi$
- $□≡◊\Box \phi \equiv \neg \Diamond \neg \phi$
  
  $□\Box$ 读作always，表明在此刻起开端会一向满意 $\phi$
这些算子是有优先级的， $,◯\neg,\bigcirc$ 优先履行，其次是 $⋃\bigcup$ ，然后是 $∨,∧\vee,\wedge$ ，最后是 $→\to$
对算子的直观解说：

在一条轨道上，假如从某时间起，每个时间只满意 $b$ ，即便没出现过 $a$ ，那么该时间也满意 $\bigcup b$
此刻，让咱们用LTL语言表达互斥现象和饥饿自在在每个时间的逻辑：
- 互斥现象： $□(c1∧c2)\Box \neg(c_1 \wedge c_2)$
- 饥饿自在： $(□◊w1⇒□◊c1)∧(□◊w2⇒□◊c2)(\Box \Diamond w_1 \Rightarrow \Box \Diamond c_1) \wedge (\Box \Diamond w_2\Rightarrow \Box \Diamond c_2)$
$□◊w1\Box \Diamond w_1$ 了解方法：先看最外层，把 $◊w1\Diamond w_1$ 看作一个 $\phi$ ，则 $□\Box \phi$ 表明在此刻起开端会一向满意 $\phi$ ；再看内层 $◊w1\Diamond w_1$ ，表明无限常常次满意 $w_1$ ；因而，加起来表明，在此刻起开端会一向无限常常次满意 $w_1$

LTL的语义

由LTL公式 $\varphi$ 在AP上引起的LT性质为： $Words()={∈(2AP)∣⊨}Words(\varphi)=\{\sigma \in (2^{AP})^\omega |\sigma \vDash \varphi \}$ ，其间 $\sigma$ 是一个轨道， $=A0A1A2⋯\sigma=A_0A_1A_2\cdots$ ，由这个LT性质能够推出如下性质：
- $⊨true\sigma \vDash true$ ，表明途径 $\sigma$ 必定有一条正确的途径
- $⊨a,iffa∈A0(i.e.,A0⊨a)\sigma \vDash a,iff \ a\in A_0(i.e.,A_0 \vDash a)$ ，表明当且仅当 $a$ 是状况调集 $A_0$ 当中的一种或许时，途径 $\sigma$ 中包括 $a$
  
  $A_0$ 包括了初始状况一切的或许， $a$ 仅仅其间的一种
- $⊨1∧,iff⊨1and⊨2\sigma \vDash \varphi_1 \wedge \varphi,iff \ \sigma \vDash \varphi_1 \ and \ \sigma \vDash \varphi_2$ ，表明假如途径 $\sigma$ 中包括了状况 $1\varphi_1$ 和 $2\varphi_2$ ，那么 $\sigma$ 包括 $1∧2\varphi_1 \wedge \varphi_2$
  
  $i . e .$ 表明“也就是”
- $⊨,iff⊭\sigma \vDash \neg \varphi,iff \ \sigma \nvDash \varphi$
- $⊨◯,iff[i..]=A1A2A3⋯⊨\sigma \vDash \bigcirc \varphi,iff \ \sigma[i..]=A_1A_2A_3\cdots\vDash \varphi$
  
  $[i..]=AiAi+1Ai+2⋯\sigma[i..]=A_iA_{i+1}A_{i+2}\cdots$ ，表明从索引 $i$ 开端后的 $\sigma$ 的后缀
- $⊨◊,iff∃j⩾0.[j..]⊨\sigma \vDash \Diamond \varphi,iff \ \exists j \geqslant 0.\sigma [j..]\vDash \varphi$
- $⊨□,iff∀j⩾0.[j..]⊨\sigma \vDash \Box \varphi,iff \ \forall j \geqslant 0.\sigma [j..]\vDash \varphi$
- $⊨□◊,iff∀j⩾0.∃⩾[i..]⊨\sigma \vDash \Box\Diamond \varphi,iff \ \forall j \geqslant 0.\exists \geqslant \sigma [i..]\vDash \varphi$
- $⊨◊□,iff∃j⩾0.∀⩾[i..]⊨\sigma \vDash \Diamond\Box \varphi,iff \ \exists j \geqslant 0.\forall \geqslant \sigma [i..]\vDash \varphi$
典范：
依据上图，咱们能够推出这个TS的四个性质：
- 从初始状况开端，每一个状况都满意 $a$ ，即 $\vDash \Box a$
- 从初始状况开端，每一个状况都满意，假如该状况不满意 $b$ ，则该状况满意 $\wedge \neg b$ ，即 $\vDash \Box (\neg b \Rightarrow \Box(a \wedge \neg b))$
- 从左面的初始状况 $s_1$ 开端，下一个状况能够一起满意 $a$ 和 $b$ ，但从右边的初始状况开端， $s_3$ 的下个状况仍是 $s_3$ ， $s_3$ 并不能一起满意 $a$ 和 $b$ ，因而 $\nvDash \bigcirc (a \wedge b)$
- 从左面的初始状况 $s_1$ 开端，每一个状况都满意 $b$ ，直到满意 $\wedge \neg b$ 时，不再满意 $b$ ，但从右边的初始状况开端，并不满意，因而 $\nvDash b \bigcup(a \wedge \neg b)$

用LTL表明咱们常见的性质

可达性（Reachability）
- 简单的可达性（simple reachability）： $◊\Diamond \psi$
- 多条件的可达性（conditional reachability）： $⋃\phi \bigcup \psi$
TS体系能够既不满意 $◊a\Diamond a$ 也不满意 $◊a\neg \Diamond a$ ：
安全性（Safety）：
- 不变性（invariant）： $□\Box \phi$
活性（Liveness）： $□(⇒◊)andothers\Box(\phi \Rightarrow \Diamond \psi) and \ others$
公正性（Fairness）： $□◊andothers\Box \Diamond \phi \ and \ others$
等价性（Equivalence）：假如 $Words()=Words()Words(\phi)=Words(\psi)$ ，那么 $\phi$ 和 $\psi$ 等价，表明为 $≡\phi \equiv\psi$
对偶性规律（Duality law）：
- $□≡◊\neg \Box \phi \equiv \Diamond \neg \phi$
- $◊≡□\neg \Diamond \phi \equiv \Box \neg \phi$
- $◯≡◯\neg \bigcirc \phi \equiv \bigcirc \neg \phi$
对偶性规律（Idempotency law）：
- $□□≡□\Box \Box \phi \equiv \Box \phi$
- $◊◊≡◊\Diamond \Diamond \phi \equiv \Diamond \phi$
- $⋃(⋃)≡⋃\phi \bigcup ( \phi \bigcup \psi) \equiv \phi \bigcup \psi$
- $(⋃)⋃≡⋃(\phi \bigcup \psi) \bigcup \psi \equiv \phi \bigcup \psi$
吸收律（Absorption law）：
- $◊□◊≡□◊\Diamond \Box \Diamond \phi \equiv \Box \Diamond \phi$
- $□◊□≡◊□\Box \Diamond \Box \phi \equiv \Diamond \Box \phi$
散布律（Distribution law）：
- $◯(⋃)≡(◯)⋃(◯)\bigcirc(\phi \bigcup \psi) \equiv (\bigcirc \phi) \bigcup (\bigcirc \psi)$
- $◊(∨)≡◊∨◊\Diamond(\phi \vee\psi) \equiv \Diamond \phi \vee \Diamond \psi$
- $□(∧)≡□∧□\Box(\phi \wedge \psi) \equiv \Box \phi \wedge \Box \psi$
留意：
- $◊(⋃)≡(◊)⋃(◊)\Diamond(\phi \bigcup \psi) \not\equiv (\Diamond\phi) \bigcup (\Diamond\psi)$
- $◊(∧)≡◊∧◊\Diamond(\phi \wedge \psi) \not\equiv \Diamond\phi \wedge \Diamond\psi$
- $□(∨)≡□∨□\Box(\phi \vee \psi) \not\equiv \Box \phi \vee \Box \psi$
- 下面的这个例子说明晰 $◊(a∧b)≡◊a∧◊b\Diamond(a \wedge b) \not\equiv \Diamond a \wedge \Diamond b$ ：
  $TS⊭◊(a∧b)TS\nvDash \Diamond(a \wedge b)$ ，但 $TS⊨◊a∧◊b)TS\vDash \Diamond a \wedge \Diamond b)$
扩展律（Expansion laws）：
- $⋃≡∨(∧◯(⋃))\phi \bigcup \psi \equiv \psi \vee ( \phi \wedge \bigcirc ( \phi \bigcup \psi))$
- $◊≡∨◯◊))\Diamond \phi \equiv \phi \vee \bigcirc \Diamond \phi))$
- $□≡∧◯□))\Box \phi \equiv \phi \wedge \bigcirc \Box \phi))$

在这篇文章里有对这几个特性的详尽介绍：blog.csdn.net/qq_37400312…

公正性（Fairness）

界说：一条途径履行过程中一切过程均契合实际状况，则表明这个途径具有了公正性。
- 关于不满意公正性的途径，能够将不合实际的状况过程剔除，途径便具有了公正性。
- 无饥饿性通常是在公正性的条件下发生的。
- 公正性通常是树立活性问题的必要手法。
生活实例：
- 关于十字路口的两个红绿灯进程进程交错履行： $TS = TrLight_1||TrLight_2$ ，给定一个活性性质的自然语言描绘为：每个红绿灯都无限常常次处于绿灯的状况。这条性质表明红绿灯在无限次状况转化的过程中，会有无限次处于绿灯的状况。
  - 轨道： ${red1,red2},{green1,red2},{red1,green2},{green1,red2}⋯\{red_1,red_2\},\{green_1,red_2\},\{red_1,green_2\},\{green_1,red_2\}\cdots$ ，像这样的轨道，满意方才咱们所说的活性，那么这条轨道也具有安全性。
  - 轨道： ${red1,red2},{green1,red2},{red1,red2},{green1,red2}⋯\{red_1,red_2\},\{green_1,red_2\},\{red_1,red_2\},\{green_1,red_2\}\cdots$ ，像这样的轨道，第二个红绿灯永远为赤色，不满意方才咱们所说的活性，那么这条轨道不具有安全性。

公正性束缚（Fairness constraints）

解说：一个程序，有一些途径永远不会履行，那么，不论这些途径履行后是正确仍是过错，咱们都不需求去验证它，所以咱们在验证的过程中，需求加上一些束缚，来避免咱们去验证一些永远不会走的途径，这个束缚，咱们称之为公正性束缚
基于动作的公正性用A-fair表明，有三种状况：无条件公正性、强公正性、弱公正性
- 关于一个没有初始状况的 $(S,Act,\to,I,AP,L)$
  - 无初始状况
  - $\subseteq Act$
  - 无限履行片段 $=s0→0s1→1s2⋯\rho = s_0 \overset{\alpha_0}{\rightarrow} s_1 \overset{\alpha_1}{\rightarrow} s_2\cdots$
- 无条件公正性束缚（Unconditional A-fair）：若轨道满意无条件公正性束缚，则 $A$ 中存在的一个或多个动作能够无限常常次履行。
  - 解说：当 $\rho$ 是一个无条件公正性途径时，关于 $A$ 中的动作在这条途径上无限常常此履行，比方 $A={}⊆Act{NC,W,C},=s0→NCs1→Ws2→Cs3→NC⋯sn→NC⋯sm→NC⋯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$ ，动作 $N C$ 在途径上常常次履行，这个途径就叫做无条件公正途径
  - 公式： $\Rightarrow \forall k \geqslant 0,\exist j \geqslant k,\alpha_j \in A$ 对轨道中的动作序列的任一方位 $k$ ，总能在 $k$ 上或 $k$ 后边找到一个方位 $j$ ，该方位的动作 $j∈A\alpha_j \in A$
- 强公正性（Strongly A-fair）：若轨道满意强公正性束缚，假如 $A$ 中存在的动作无限常常次想要履行，则会导致 $A$ 中存在一个或多个动作能够无限常常次履行。
  - 公式： $\forall k \geqslant 0,\exist j \geqslant k,Act(s_j) \cap A \neq \varnothing ) \Rightarrow \forall k \geqslant 0,\exist j \geqslant k,\alpha_j \in A$ 对轨道中的状况序列的任一方位 $k$ ，若总能在 $k$ 上或 $k$ 后边找到一个方位 $j$ ，使得状况 $s_j$ 的一切直接动作 $Act(s_j)$ 中存在 $A$ 中的动作（即 $Act(sj)∩A≠∅Act(s_j) \cap A \neq \varnothing$ ，无限常常次想要履行），那么 $A$ 中必定存在无限常常次履行的动作
- 弱公正性（Weakly A-fair）：若轨道满意弱公正性束缚，假如 $A$ 中的某时间开端，无限常常次有 $A$ 中的动作想要履行，则会导致 $A$ 中存在一个或多个动作能够无限常常次履行。
  - 公式： $\exist k \geqslant 0,\forall j \geqslant k,Act(s_j) \cap A \neq \varnothing ) \Rightarrow \forall k \geqslant 0,\exist j \geqslant k,\alpha_j \in A$ 对轨道中的状况序列的某一方位 $k$ ，若总能在 $k$ 上或 $k$ 后边找到一个方位 $j$ ，使得状况 $s_j$ 的一切直接动作 $Act(s_j)$ 中存在 $A$ 中的动作（即 $Act(sj)∩A≠∅Act(s_j) \cap A \neq \varnothing$ ，无限常常次想要履行），那么 $A$ 中必定存在无限常常次履行的动作
  其间， $\{ \alpha \in Act | \exist s’ \in S,s\overset{\alpha}{\rightarrow} s’ \}$
- 例题一：
  - 取动作 $A=\{enter_1,enter_2 \}$ ，判别下面的赤色轨道是否满意强公正性？（赤色轨道从第2个方位开端，234方位的状况轮以闭圈的方式无限次履行）
  - 答案：
    - 在赤色轨道中，咱们看到，状况 $⟨w1,n2,y=1⟩\left \langle w_1,n_2,y=1 \right \rangle$ 无限次想要履行 $enter_1$ ，状况 $⟨w1,w2,y=1⟩\left \langle w_1,w_2,y=1 \right \rangle$ 无限次想要履行 $enter_1$ 和 $enter_2$ ，轨道终究的成果是无限常常次履行 $enter_2$ ，所以这个轨道满意强公正性。
- 例题二：
  - 取动作 $A=\{req_2 \}$ ，判别下面的赤色轨道是否满意弱公正性？（赤色轨道从第1个方位开端，123方位的状况轮以闭圈的方式无限次履行）
  - 答案：
    - 在赤色轨道中，咱们看到，从第一个状况开端，每一个状况都无限常常次想要履行 $req_2$ ，但 $A$ 中不存在无限常常次履行的动作，所以这个轨道不满意弱公正性。
程序或进程在无条件公正性下停止的状况： $procInc=while⟨x⩾0dox:=x+1⟩odprocReset=x:=−1\begin{aligned} proc \ Inc \ =& \ while \ \left \langle x \geqslant 0 \ do \ x := x + 1 \right \rangle \ od \\ proc \ Reset \ = & \ x := −1 \end{aligned}$

$x$ 是共享变量，初始值为0
公正性对途径的束缚过强或过弱
- 公正性的目的是扫除“不合理”的途径，但假如咱们去除了过度或者取出缺乏时，对验证成果会发生必定的影响。
- 束缚过强（去除过度时）：
  - 总的途径 $⊆\subseteq$ 合理的途径 $⊆\subseteq$ 验证用的途径
  - 假如验证成果为false，则能够说明合理的途径对应的模型是有问题的
  - 假如验证的成果为true，无法说明合理的途径对应的模型是正确的
- 束缚过弱（去除缺乏时）：
  - 总的途径 $⊆\subseteq$ 验证用的途径 $⊆\subseteq$ 合理的途径
  - 假如验证成果为true，则能够说明合理的途径对应的模型是正确的
  - 假如验证的成果为false，无法说明合理的途径对应的模型是过错的

关于公正性的这部分，我在另一篇文章里进行了解说，但为了方便了解关于LTL的公正性束缚问题，我有将这部分内容从头粘贴了过来，另一篇文章的链接为：blog.csdn.net/qq_37400312…

LTL的公正性束缚

假定 $\phi$ 和 $\psi$ 是在AP上的出题逻辑公式，则

无条件的LTL公正性束缚的方式如下： $\Box \Diamond \psi$
强LTL公正性束缚的方式如下： $\Box \Diamond \phi \to \Box \Diamond \psi$ ，从此刻起每时每刻都会想要在未来某时间想要履行 $\phi$ ，则从此刻起每时每刻都会能够在未来某时间能够履行 $\psi$
弱LTL公正性束缚的方式如下： $\Diamond \Box \phi \to \Diamond \Box \psi$ ，在未来某一时间起会一向想要履行 $\phi$ ，则在在未来某一时间会一向能够履行 $\psi$

$\phi$ 表明想要履行， $\psi$ 表明能够履行

LTL的公正性假定

强公正性假定： $sfair=⋃0<i⩽k(□◊i→□◊i)sfair=\underset{0<i\leqslant k}{\bigcup}(\Box\Diamond \phi_i \to \Box\Diamond \psi_i)$
通用格局： $fair \wedge sfair \wedge wfair$
经验规律：强或无条件公正性假定有利于处理争议，弱的公正性足以处理由交织发生的不决定性

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

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

线性时态逻辑：以状况开端的（一切）途径的句子。例如:
- $\vDash \Box(x \leqslant 20)$ ，表明从s开端的一切途径都满意 $x⩽20x\leqslant 20$
分支时态逻辑：关于以一个状况开端的一切或某些途径的句子。例如:
- $\vDash \forall \Box (x \leqslant 20)$ ，表明从s开端的一切途径都满意 $x⩽20x\leqslant 20$
- $\vDash \exists \Box (x \leqslant 20)$ ，表明从s开端存在途径满意 $x⩽20x\leqslant 20$

检查LTL中是否有 $∃\exists \varphi$ ，能够用CTL的 $∀\forall \neg \varphi$ 检测

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

Transition systems：

Trees：

咱们看到，这个Transition systems有着无穷无尽的途径，咱们用数来表明各个途径，但没有办法将其悉数表明出来，图中表明晰前四次转移，尽管没有办法悉数表明，但咱们能够依据Transition systems来判别某条途径是否满意某性质。

状况和算子

状况上的句子：
- 原子出题： $\in AP$
- 否规律： $\neg \phi$
- 结合律： $∧\phi \wedge \psi$
- 存在一条实现 $\phi$ 的途径： $∃\exists \phi$
- 一切途径都能够实现 $\phi$ ： $∀\forall \phi$
途径上的句子：
- 下一个状况满意： $◯\bigcirc \phi$
- $\phi$ 一向满意直到 $\psi$ 满意： $⋃\phi \bigcup \psi$
$◯\bigcirc$ 和 $⋃\bigcup$ 会与 $∃\exists$ 和 $∀\forall$ 替换运用
派生算子：
- 存在途径满意 $\phi$ ： $∃◊≡∃(true⋃)\exists \Diamond \phi \equiv \exists(true \bigcup \phi)$
- 一切途径满意 $\phi$ ： $∀◊≡∀(true⋃)\forall \Diamond \phi \equiv \forall (true \bigcup \phi)$
- 存在途径总是满意 $\phi$ ： $∃□≡∀◊\exists \Box \phi \equiv \neg \forall \Diamond \neg \phi$
- 一切途径总是满意 $\phi$ ： $∀□≡∃◊\forall \Box \phi \equiv \neg \exists \Diamond \neg \phi$
- 弱直到： $∃(W)≡∀((∧)⋃(∧))\exists(\phi W \psi) \equiv \neg \forall ((\phi \wedge \neg \psi)\bigcup(\neg \phi \wedge \neg \psi))$ $∀(W)≡∃((∧)⋃(∧))\forall (\phi W \psi) \equiv \neg \exists((\phi \wedge \neg \psi)\bigcup(\neg \phi \wedge \neg \psi))$

语义

语义学的可视化化

CTL状况公式的语义学

$\vDash \phi$ 表明当且仅当公式 $\phi$ 在状况 $s$ 中成立

$\vDash a$ ，在 $a$ 属于从状况 $s$ 出发的途径中的一条途径时，时成立，即 $\in L(s)$
$\vDash \neg \phi$ ， $\ \neg (s \vDash \phi)$
$\vDash \neg \phi$ ， $\ (s \vDash \phi) (s \vDash \psi)$
$\vDash \exists \phi$ ， $i f f$ 从 $s$ 开端的一些途径 $\pi$ 满意 $⊨\pi \vDash \phi$
$\vDash \forall \phi$ ， $i f f$ 从 $s$ 开端的一切途径 $\pi$ 满意 $⊨\pi \vDash \phi$

CTL途径公式的语义学

$⊨\pi \vDash \phi$ 表明途径 $\pi$ 满意公式 $\phi$

$⊨◯iff[1]⊨\pi \vDash \bigcirc \phi iff \ \pi [1] \vDash \phi$
$⊨⋃iff(∃j⩾0.[j]⊨∧∀0⩽k<j.[k]⊨)\pi \vDash \phi \ \bigcup \psi \ iff \ (\exists j \geqslant 0.\pi [j] \vDash \psi \wedge \forall 0 \leqslant k <j.\pi[k]\vDash \phi)$

$[i]\pi[i]$ 表明在途径 $\pi$ 上面的状况 $s_i$

搬迁体系语义

满意CTL状况公式 $\phi$ 的调集 $Sat()Sat(\phi)$ 界说为： $Sat()={s∈S∣s⊨}Sat(\phi) =\{s \in S | s \vDash \phi \}$
当一切初始状况满意 $\phi$ 时，TS满意CTL公式： $\vDash \phi \ iff \ \forall_{s_0} \vDash \phi$

TS或许不满意 $\phi$ 也不满意 $\neg \phi$ ，即 $\nvDash \phi \ and \ TS \nvDash \neg \phi$

CTL的一些常用性质

等价性（equivalence）：假如两个CTL: $\phi$ 和 $\psi$ 的 $Sat()=Sat()Sat(\phi)=Sat(\psi)$ ，则 $\phi$ 和 $\psi$ 等价，即 $≡\phi \equiv \psi$ $≡iffTS⊨∧TS⊨\phi \equiv \psi \ iff \ TS \vDash \phi \wedge TS \vDash \psi$
扩展律（Expansion laws）
- $∀(⋃)≡∨(∧∀◯∀(⋃))\forall (\phi \bigcup \psi) \equiv \psi \vee (\phi \wedge \forall \bigcirc \forall (\phi \bigcup \psi))$
- $∀◊≡∨∀◯∀◊\forall \Diamond \phi \equiv \phi \vee \forall \bigcirc \forall \Diamond \phi$
- $∀□≡∧∀◯∀□\forall \Box \phi \equiv \phi \wedge \forall \bigcirc \forall \Box \phi$
- $∃(⋃)≡∨(∧∀◯∀(⋃))\exists (\phi \bigcup \psi) \equiv \psi \vee (\phi \wedge \forall \bigcirc \forall (\phi \bigcup \psi))$
- $∃◊≡∨∃◯∃◊\exists \Diamond \phi \equiv \phi \vee \exists \bigcirc \exists \Diamond \phi$
- $∃□≡∧∃◯∃□\exists \Box \phi \equiv \phi \wedge \exists \bigcirc \exists \Box \phi$
散布律（Distributive laws）
- $∀□(∧)≡∀□∧∀□\forall \Box(\phi \wedge \psi) \equiv \forall \Box \phi \wedge \forall \Box \psi$
- $∃◊(∨)≡∃◊∨∃◊\exists \Diamond (\phi \vee \psi) \equiv \exists \Diamond \phi \vee \exists \Diamond \psi$
- $∃□(∧)≡∃□∧∃□\exists \Box(\phi \wedge \psi) \not\equiv \exists \Box \phi \wedge \exists \Box \psi$
- $∀◊(∨)≡∀◊∨∀◊\forall \Diamond (\phi \vee \psi) \equiv \forall \Diamond \phi \vee \forall \Diamond \psi$

【系统分析与验证笔记】线性时态逻辑LTL和计算树逻辑CTL

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

线性时间特点（LT property）

LTL的语法

LTL的语义

用LTL表明咱们常见的性质

公正性（Fairness）

公正性束缚（Fairness constraints）

LTL的公正性束缚

LTL的公正性假定

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

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

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

状况和算子

语义

语义学的可视化化

CTL状况公式的语义学

CTL途径公式的语义学

搬迁体系语义

CTL的一些常用性质

作者信息

【系统分析与验证笔记】 线性时态逻辑LTL和计算树逻辑CTL

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

线性时间特点（LT property）

LTL的语法

LTL的语义

用LTL表明咱们常见的性质

公正性（Fairness）

公正性束缚（Fairness constraints）

LTL的公正性束缚

LTL的公正性假定

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

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

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

状况和算子

语义

语义学的可视化化

CTL状况公式的语义学

CTL途径公式的语义学

搬迁体系语义

CTL的一些常用性质

相关文章

python脚本第一弹——Excel处理

AI开发实践：关于停车场中车辆识别与跟踪

Spring MVC 之 ViewResolver

资源画像，看得见的容器资源优化助手

作者信息

【系统分析与验证笔记】线性时态逻辑LTL和计算树逻辑CTL