Page 167 - 《软件学报》2025年第8期

3590 软件学报 2025 年第 36 卷第 8 期

时序逻辑 (signal temporal logic, STL) [33] 可以描述连续时间下系统中的实值信号的属性, 常用于描述包含连续行为
的 CPS 系统的行为规约. 混成自动机及信号时序逻辑的形式化定义如下.
定义 1. 混成自动机. 混成自动机可以由一个多元组 H = (X,Q,F,Inv,E,G,R,Q ,Q ) 定义, 其中,
f
0
1) X 是连续变量的集合;
2) Q 是离散节点的集合, 其中,
˙ X = F q (X);
• 流函数 F = {F q |q ∈ Q} 定义各个离散节点下连续变量的动态行为, 通常为微分方程
• 不变式 Inv = {Inv q |q ∈ Q} 定义各个离散节点下连续变量需要满足的不变式约束 Inv q (X);
3) E ⊆ Q× Q 是离散节点的跳转集合, 其中,
• 转移卫式 G = {G e |e ∈ E} 定义各个离散跳转发生时连续变量需要满足的约束 G e (X);
• 重置条件 R = {R e |e ∈ E} 定义各个离散跳转发生后连续变量需执行的重置动作 X := R e (X);
0
4) Q 是初始节点的集合, 表示系统可以从哪些离散节点开始;
f
5) Q 是终止节点的集合, 表示系统的目标节点或接收节点.
混成自动机的状态由当前所处的离散节点以及当前连续变量的取值两者决定, 可由二元组 s = (q, x) ∈ S 表示,
其中, S = Q× X 为混成自动机的状态空间. 混成自动机在状态 s = (q, x) 下有两种可能的行为: 可以继续停留在节
q 下 e = (q,q ) ∈ E 跳到节
′
点 (需满足不变式约束 Inv q ), 变量根据流函数 F q 随时间连续变化; 也可以沿着离散跳转
′
点 (需满足转移卫式 G e ), 变量根据重置条件 R e 更新, 状态即刻变化为 (q ,R e (x)).
定义 2. 路径. 混成自动机 H = (X,Q,F,Inv,E,G,R,Q ,Q ) 的路径是由离散节点构成的序列 p = {q i } , 其中,
N
0
f
0
f
• 序列从初始节点开始, 由终止节点结束, 即: q 0 ∈ Q ,q N ∈ Q ;
0
• 对于序列上任意两相邻节点, 自动机中都存在从前者跳到后者的跳转, 即: ∀i ∈ [0,N),(q i ,q i+1 ) ∈ E.
混成自动机的路径描述了系统在离散状态空间中的演化序列, 但并未涉及混成自动机的状态在各个节点下随
时间连续变化的过程. 因此, 只有进一步给定系统变量的初始值 x 0 以及系统在离散路径 p 中的每个节点上停留的
时间 τ 时, 混成自动机的动态行为才可以被完整定义且唯一确定.
N
N
值得注意的是, 并不是任意的三元组 (x 0 , p = {q i } ,τ = {τ} ) 都对应混成自动机上的合法行为. 只有当系统按照
0 0
给定变量初值 x 0 , 路径 p, 以及节点停留时间 τ 运行, 节点上的不变式约束以及跳转上的转移卫式约束从未被违背
时, 该三元组才定义了一个合法的系统行为. 下面给出混成自动机上的合法行为的形式化定义.
定义 3. 合法行为. 在混成自动机 H = (X,Q,F,Inv,E,G,R,Q ,Q ) 中, 给定 x 0 为变量 X 的初值, p = {q i } N 为混成
0
f
0
自动机的路径, τ = {τ i } N 为在路径 p 的每个节点上的停留时间, 令此时混成自动机 H 根据其流函数 F 及重置条件
0
R 运行的行为轨迹为 w S : [0,τ N ] → Q× X, 则行为 w S = (w Q ,w X ) 是 H 中的合法行为当且仅当:
(x 0 ,p,τ) (x 0 ,p,τ) (x 0 ,p,τ) (x 0 ,p,τ)
• 在每个节点下, 状态总满足 H 中相应的不变式约束, 即: (w X (t));
(x 0 ,p,τ)
∀i ∈ [0,N],∀t ∈ [τ i ,τ i+1 ),Inv q i
• 每次跳转时, 状态总满足 H 中相应的转移卫式约束, 即: ∀i ∈ [0,N),G (q i ,q i+1 ) (w X (τ i+1 )) 总成立.
(x 0 ,p,τ)
在本文中, 我们用符号 C p 表示上述路径 p 上的系统合法行为需要满足的所有不变式和转移卫式约束.
n
定义 4. 信号时序逻辑. 给定 X 为 R 上定义的 n 维变量 ( R = R∪{⊤,⊥} 为包含所有实数和布尔值的扩展实数
n
X
X
域, ⊤,⊥ 分别为最大和最小元素), 信号 w : T → R 为变量 X 在时间域 T = [0,t) ⊆ R 上的值, 则表示信号 w 的时序性
n
质的信号时序逻辑公式的语法为: φ := true|θ(X) ⩾ d|¬φ 1 |φ 1 ∨φ 2 |φ 1 U I φ 2 . 其中, θ : R → R 是将变量 X 映射到实数的
函数, d ∈ R 是常数; U 是表示“直到 (Until)”的时序算子, 其下标 I ⊆ R 表示时间区间, I = [0,∞) 时可省略. 其他常
+
见的逻辑常数, 逻辑连接词和时序算子都可以用该语法表示, 譬如: false ≡ ¬true, φ 1 ∧φ 2 ≡ ¬(¬φ 1 ∨¬φ 2 ), φ 1 → φ 2 ≡
¬φ 1 ∨φ 2 , F I φ ≡ trueU I φ, G I φ ≡ ¬(F I ¬φ), φ 1 R I φ 2 ≡ ¬(¬φ 1 U I ¬φ 2 ) 等.
信号时序逻辑公式具有布尔语义和定量语义 [15,16] , 其递归定义如表 1. 其中, 布尔语义描述信号 w 在给定时刻
t
t 是否满足公式 φ, 定量语义 ρ(φ,w,t) 则描述信号 w 在时刻 满足公式 φ 的程度 (鲁棒性). 鲁棒性为正表示信号满
足公式, 鲁棒性为负则表示信号不满足公式, 并且值越小表示信号满足公式的程度越低. 其中, 在信号初始时刻 (即
t = 0 时), 信号的鲁棒性 ρ(φ,w,0) 通常被简写为 ρ(φ,w).