论文阅读笔记——信息物理系统时空逻辑研究(未完待续)

Reference

[1] 邵珠成. 信息物理系统时空逻辑研究[D].华东师范大学,2013.

Main Ideas

（1）这篇论文为了描述这些具有时间和空间特征的逻辑属性和行为约束，根据PTL(命题时态逻辑)、$S4_u$ 和扩展逻辑语言的方法，构造了一种具有时空特征的逻辑语言。

（2）基于这种逻辑语言，对混成系统在空间变量和空间表达式方面进行扩展，构造时空自动机模型，并给出相关语义。

（3）以具体案例进行系统建模、语义描述、性质描述。

CPS

CPS（Cyber-Physical System）是一个综合计算、网络和物理环境的多为复杂系统，通过3C（即计算-Computation、通信-Communication和控制-Control）技术的有机融合与深度协作，实现大型工程系统的实时感知、动态控制和信息服务。本质上说，CPS是一个具有控制功能的网络。

特点：

（1） CPS系统具有连续的计算过程和离散的计算过程，两者相互交织；

（2） CPS也是一个智能的有自主行为的系统，能够从环境中获取相关数据，并进行数据融合、有效信息提取等。

（3） CPS系统的多样性决定了它可以应用在广泛的领域。

Temporal logic and Spatial logic

时态逻辑和空间逻辑。

时态逻辑

时态逻辑是一种用于描述为了表示和推理根据时间限定的命题所使用的任意规则和符号系统。

PTL（命题时态逻辑）被解释为命题变量随着时间流的变化。

PTL，命题时态逻辑公式可以定义为：

p 是命题变量。

𝒰 和𝒮 是二元时态操作符。

模型：

第一个符号是一个时间流；

第二个符号表示一个映射，它将每一个命题变量𝑝 映射到一个时间点的集合，该集合⊆ 𝑊。

空间逻辑

空间逻辑是用来表示事物所存在的空间位置及其事物之前的位置关系的。

$S4_u$ 是表达能力最强的一种空间逻辑，是由命题模态逻辑S4 通过扩展存在量词和全称量词而来。

S4 的公式定义为：

$S4_u$ 的公式定义为：

𝜏 是一个空间区域。

给定一个区域𝜏 , 对于∃𝜏，我们认为被𝜏 所表示的这个空间区域是非空（也就是

说，至少有一个点存在于𝜏 中）。

∀ 𝜏 意思是说，𝜏 占有整个空间区域（所有的点都在𝜏 中），并且有

模型：

I = ⟨𝑈，Ⅱ⟩ 是一个拓扑逻辑空间。

第二个符号表示一个映射，它将每个变量𝑝 映射到一个集合，该集合⊆ U。

逻辑组合

使用时态逻辑T对逻辑系统L进行时态化扩充，使其具有时序特征。

Spatiotemporal logic

时空逻辑。

p 是关于属性的普通命题变量；

𝜏 是位置相关的空间变量；

I𝜏 是作用于空间变量𝜏 上的模态操作符；

𝒰 和𝒮 是二元时态操作符。

模型：

分别表示时间流、一个拓扑空间、一个映射（它可以将每个空间变量𝑠 在每个时间点𝑤 ∈ 𝑊 的值映射到一个集合）

Spatio-Temporal Hybrid Automata

时空混成自动机。

时空混成自动机是基于时空逻辑由混成自动机扩展而来。由于将时空逻辑引入混成自动机，使其具有了对信息物理系统中位置或者空间相关信息的表达能力。

模型：

一个时空自动机模型可以被表示为一个七元组：

M-有限状态集；

X-连续状态空间；

A-有限集，状态转换的边的标签集合；

Var-变量集；

E-迁移；

Inv-不变式；

Act-模式的活动，描述连续变量随时间变化的情况。

状态：

时空混成自动机的执行过程，既有离散的模式转变，又有连续的状态转换。这种混成的离散连续动态行为可以被形式化的定义为一个完全是离散的转移系统。

在时空混成自动机中，一个系统的状态可以被形式化的定义为一个多元组：

-𝑚 ∈ 𝑀 是模式名称，它描述当前系统执行所在的模式为𝑚。

-𝑣𝑉𝑎𝑟 → 𝑣𝑎𝑙𝑢𝑒 表示系统状态中每个变量的取值。其中，𝑣𝑎𝑙𝑢𝑒 是𝑉𝑎𝑟 的值域。每个在𝑉𝑎𝑟 中的变量都取一个值。

-𝑖 是一个时间序列，它表示当前状态所使用时钟对应的时间点序列。

-𝜄 = $𝐿𝑜𝑐_𝑖$(𝑚) 记录了模式𝑚 在当前时间序列𝑖 下的位置信息。对于时间序列中的每个时间点，该函数都会记录该系统状态下各个模式的位置信息。

时空逻辑扩充了时态逻辑系统在空间命题相关的表达能力，而空间命题的表达能力恰恰是信息物理系统所必需的。对于建模系统的行为，时空混成自动机扩充了混成自动机对空间变量及表达式方面的表达和计算能力，可以有效的对CPS进行建模。对于CPS系统的验证问题，在利用时空混成自动机进行行为建模的基础上，时空逻辑可以对系统的性质进行描述，这是进行模型验证的基础工作。