形式化语言——时序逻辑

时序逻辑

在模型检测工具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中搜索大佬写的博客。

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

1.1 kripke structure 定义 1

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

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

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

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

2. 线性时序逻辑（LTL）

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

在这里插入图片描述

2.1 特点

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

2.2 构成

项（terms）： $p$ 表示原子命题
经典布尔操作
- $\neg$ （not）
- $\vee$ （or）
- $\wedge$ （and）
- $\rightarrow$ （imply, if-then）： $p\rightarrow q$ ，如果 $p$ 发生则会出现 $q$
基本时态操作（Basic temporal operators）
- $\square$ （G, always）
  - $\square p$ ： $p$ holds globally in the future.
  - 从当前时刻起， $p$ 总是为真
- $\diamond$ （F, eventually）
  - $\diamond p$ ： $p$ holds sometime（不确定性！）in the future
  - $p$ 在以后某个时刻会真
- $\circ$ （X, next）
  - $\circ p$ ： $p$ holds next time.
  - $p$ 在下一个时刻为真
- $\cup$ （strong unit）
  - $\cup q$ ： $p$ holds until $q$ holds.

2.3 例子（红绿灯）

以红绿灯为例。

$g r$ ：green
$ye$ ：yellow
$re$ ：red

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

对应的LTL： $\square ( (gr\cup ye) \vee (ye \cup re) \vee (re \cup gr) )$

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

对应的LTL： $\square ( \neg(gr \vee ye) \wedge \neg (ye \vee re) ∧ \neg (re \wedge gr) \wedge (gr \vee ye \vee 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 是一个三元组，记作 $Fl=\left \langle I_{Fl},T_{Fl},Init_{Fl} \right \rangle$ ，其中 $I_{Fl},T_{Fl} \in Act$ 分别表示它的发起动作集合和终止动作集合， $Init_{Fl}$ 代表 $F_l$ 的初始真值。

2.4.1.2 Fluent 解释

对于一个 $F_l=\left \langle I_{Fl},T_{Fl},Init_{Fl} \right \rangle$ 来说，显然有 $I_{Fl} \cap T_{Fl} = \empty$ 。例如，每一个动作 $\in Act$ 可以导出一个对应的 fluent 记为 $\ { l } , f a l s e ⟩ \dot l = \left \langle l,Act \verb|\| \{l\},false \right \rangle$ 。这个表示说，当动作 $l$ 发生的时候， $\dot l$ 为真，发生任何其他动作的时候，这个 fluent 为假。

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

2.4.2 $\pi,i \vDash Fl$

2.4.2.1 $\pi,i \vDash Fl$ 定义

一个 $\pi = l_0,l_1,...$ 在位置 $i$ 处满足一个 $\thinspace Fl$ ，记作 $\pi,i \vDash Fl$ ，当且仅当以下的条件至少有一个成立：

$Init_{Fl} \wedge (\forall j \in N \cdot 0 \leq j \leq i \rightarrow l_i \notin T_{Fl})$
$\exist j \in N \cdot (j \leq i \wedge l_j \in I_{Fl}) \wedge (\forall k \in N \cdot j∃j∈N⋅(j≤i∧lj∈IFl)∧(∀k∈N⋅j<k≤i→lk∈/TFl)$

2.4.2.2 $\pi,i \vDash Fl$ 解释

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

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

在这里插入图片描述

在 图2-1 中的客户端 LTS Cli 中，我们可以定义 $\thinspace CALLING=\left \langle \{call\},\{display\},flase \right \rangle$ 来表示客户端是否请求服务。对于一个 $\thinspace \pi_{0}=getToken,call,reply,display,...$ ，我们可以看到有 $\pi_0,1 \vDash CALLING$ ，因为这是遇到了 call 动作，但是还没有遇到 display 动作。

类似地，我们还可以得到 $\pi_0,3 \nvDash CALLING$ 。

2.4.3 合法的 FLTL 公式

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

任意的 $\thinspace F_l \in \digamma$ 是一个合法的 FLTL 公式，
如果 $\phi$ 和 $\psi$ 是合法的 TLTL 公式，那么 $\neg \phi$ ， $\phi \vee \psi$ ， $X\phi$ ， $\phi U \psi$ 也都是合法的 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 $\pi,i \vDash \phi$

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.
1

给定一个无穷 $\thinspace \pi$ ，其是否在位置 $i$ 满足公式 $\phi$ ，记为 $\pi,i \vDash \phi$ 。

如果 $\neg(\pi,i \vDash \phi)$ ，则 $\pi,i \vDash \neg \phi$
如果 $(\pi,i \vDash \phi) \vee(\pi,i \vDash \psi)$ ，则 $\pi,i \vDash \phi \vee \psi$
如果 $\pi,i+1 \vDash \phi$ ，则 $\pi,i \vDash X \phi$
如果 $\exists j \geq i \cdot \pi,j \vDash \psi \wedge \forall i \leq k < j \cdot \pi,k \vDash \phi$ ，则 $\pi,i \vDash \phi U \psi$

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

2.4.5 $\vDash \phi$

2.4.5.1 $\vDash \phi$ 定义

一个 $\thinspace \pi$ 满足公式 $\phi$ 记为 $\pi \vDash \phi$ ，如果有 $\pi,0 \vDash \empty$ 。

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

2.4.5.2 $\vDash \phi$ 例子

在这里插入图片描述

总是在请求服务（call 动作）之后，能够把结果展示出来（display动作）。那么这样的一个性质可以用 FLTL 公式表示成： $DISPLAY\_AFTER\_CALL=\square (call\rightarrow \diamond display)$ 。显然，我们可以看出来有 $\pi_0 \vDash DISPLAY\_AFTER\_CALL$ 以及 $\vDash DISPLAY\_AFTER\_CALL$ 。

3. 分支时序逻辑（CTL）

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

在这里插入图片描述

3.1 构成

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

路径量词：

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

时态算子：

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

常见表达：

$\forall X p$ ：在所有未来路径上，公式在下一个状态为真
$\forall F p$ ：在所有未来路径上，公式在某个状态必然为真
$\forall G p$ ：在所有未来路径上，公式都永远为真
$\forall (p U q)$ ：在所有未来路径都存在：公式 $p$ 一直为真，直到公式 $q$ 为真
$\exists X p$ ：存在一条未来路径，下一状态公式为真
$\exists F p$ ：存在一条未来路径，公式在某个状态一定为真
$\exists G p$ ：存在一条未来路径，公式永为真
$E (p U q)$ ：存在一条未来路径，公式 $p$ 一直为真，直到公式 $q$ 为真

3.2 例子

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

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

对应的CTL： $\forall G ! (proc1.state = critical \& proc2.state = critical)$

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

对应的CTL： $\forall G (proc1.state = entering \rightarrow \forall F proc1.state = critical)$

4. 状态满足公式

描述	公式
deMargan律	$\neg (\phi \wedge \psi)\equiv \neg \phi \vee \neg \psi$
	$\neg (\phi \vee \psi)\equiv \neg \phi \wedge \neg \psi$
幂等律	$\neg \neg \phi \equiv \phi$
对偶率	$\neg G \phi \equiv F \neg \phi$
	$\neg F \phi \equiv G \neg \phi$
	$\neg F (\phi U \psi) \equiv \neg \phi R \neg \psi$
	$\neg (\phi R \psi)\equiv \neg \phi U \neg \psi$
自对偶率	$\neg X \phi \equiv X \neg \phi$
分配率	$F(\phi \vee \psi) \equiv F \phi \vee F \psi$
	$G(\phi \vee \psi) \equiv G \phi \vee G \psi$
连接词相互定义	$\phi \equiv \top U \phi$
	$\phi \equiv \bot R \phi$
	$\phi W \psi \equiv \phi U \psi \vee G \phi$
	$\phi W \psi \equiv R(\phi \vee \psi)$
	$\phi R \psi \equiv \psi W(\phi \wedge \psi)$
	$\phi U \psi \equiv \phi W \psi \wedge F \psi$

相关阅读:
Python学习笔记——基本类型、函数、输入和输出
 第15章秒杀商品隔离解决方案
 TCP Illinois 与 TCP Highspeed
【ESP32】Arduino C语言语法总结
 青少年python系列 35.自定义函数
 一文读懂ChatGPT模型原理
 基于BP神经网络的电力负荷预测附Matlab代码
 SPL工业智能：发现时序数据的异常
 2023程序员HR面试面经
 【C++】-- STL之用红黑树模拟实现map和set
原文地址：https://blog.csdn.net/qq_46371399/article/details/127567705

形式化语言——时序逻辑

时序逻辑

1. kripke structure

1.1 kripke structure 定义 1

2. 线性时序逻辑（LTL）

2.1 特点

2.2 构成

2.3 例子（红绿灯）

2.4 流性线性时序逻辑

2.4.1 Fluent

2.4.1.1 Fluent 定义

2.4.1.2 Fluent 解释

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 定义

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

2.4.3 合法的 FLTL 公式

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

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

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

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

3. 分支时序逻辑（CTL）

3.1 构成

3.2 例子

4. 状态满足公式

2.4.2 $\pi,i \vDash Fl$

2.4.2.1 $\pi,i \vDash Fl$ 定义

2.4.2.2 $\pi,i \vDash Fl$ 解释

2.4.4 $\pi,i \vDash \phi$

2.4.5 $\vDash \phi$

2.4.5.1 $\vDash \phi$ 定义

2.4.5.2 $\vDash \phi$ 例子