前言：因为天天写代码实在是太枯燥了，所以读点其他东西来调剂一下，这样科研进度不至于停下。前面读了几篇关于时序逻辑学习的文章，今天来了解一下时序逻辑公式在控制中的应用。
Raman, V., Donze, A., Maasoumy, M., Murray, R. M., Sangiovanni-Vincentelli, A., & Seshia, S. A. (2014, December). Model predictive control with signal temporal logic specifications. 53rd IEEE Conference on Decision and Control. https://doi.org/10.1109/cdc.2014.7039363
概览
对系统特性做出约束是时序逻辑的作用之一。在这篇文章中，STL可以用来描述系统的safety, response, bounded liveness等多种属性。而控制器的设计要把这些属性约束考虑在内，这篇文章探讨的就是如何将形式语言转化为模型语言，即数学公式，设计控制器使得系统满足时序逻辑约束。本文把混合整数线性规划问题与模型预测控制相结合，完成了对STL公式的编码。验证实验为大楼的能源和温度控制。
流水账笔记
1 Introduction
- 将STL约束编码 转换为MILP约束
- 设计MPC控制器
- 大楼暖空的模型验证
2 Preliminary
A. Discrete-Time Continuous Systems
离散时间连续系统：采样时间是离散值，信号的状态可以取连续值。
x
t
+
1
=
f
(
x
t
,
u
t
)
x_{t+1}=f(x_t,u_t)
xt+1=f(xt,ut)
DTCS的三要素：
- 初始状态
x
0
x_0
x0
- 控制信号
u
N
=
u
0
u
1
u
2
.
.
.
u
N
−
1
\mathbf{u}^N = u_0 u_1 u_2 ... u_{N-1}
uN=u0u1u2...uN−1
- 状态轨迹(run)
x
(
x
0
,
u
N
)
=
x
0
x
1
x
2
…
x
N
\mathbf{x}\left(x_{0}, \mathbf{u}^{N}\right)=x_{0} x_{1} x_{2} \ldots x_{N}
x(x0,uN)=x0x1x2…xN
这里我们把N称作信号的边界(horizon)，代表装填轨迹的最大编号。
接下来还定义了代价函数：
J
(
x
,
u
)
J(\mathbf{x}, \mathbf{u})
J(x,u)，具体怎么用还没讲。
B. Signal Temporal Logic
参考前几篇文献对STL的定义。
另外补充bounded-time STL的时间上界(Horizon)的求取方法：
所有嵌套额时序操作子的上边界相加，表示为验证时序逻辑公式所需的最小轨迹长度。
C. Robust Satisfication of STL formulas
同这篇文献.
3 Problem Statement
基于STL的优化控制
在系统轨迹符合STL公式
φ
\varphi
φ的前提下，优化一个与系统轨迹有关的代价函数：
argmin
u
N
J
(
x
(
x
0
,
u
N
)
)
s.t.
x
(
x
0
,
u
N
)
⊨
φ
\begin{array}{ll} \operatorname{argmin}_{\mathbf{u}^{N}} & J\left(\mathbf{x}\left(x_{0}, \mathbf{u}^{N}\right)\right) \\ & \text { s.t. } \mathbf{x}\left(x_{0}, \mathbf{u}^{N}\right) \models \varphi \end{array}
argminuNJ(x(x0,uN)) s.t. x(x0,uN)⊨φ
基于STL的模型预测控制
最小化每一步的代价函数：
argmin
u
H
,
t
J
(
x
(
x
t
,
u
H
,
t
)
,
u
H
,
t
)
)
s.t.
x
(
x
0
,
u
)
⊨
φ
\begin{aligned} \operatorname{argmin}_{\mathbf{u}^{H, t}} &\left.J\left(\mathbf{x}\left(x_{t}, \mathbf{u}^{H, t}\right), \mathbf{u}^{H, t}\right)\right) \\ & \text { s.t. } \mathbf{x}\left(x_{0}, \mathbf{u}\right) \models \varphi \end{aligned}
argminuH,tJ(x(xt,uH,t),uH,t)) s.t. x(x0,u)⊨φ
这里解释一下优化控制的优化函数与MPC的优化函数的主要差别。观察前后两式，唯一不同的就在于输入信号轨迹的长度一个是
N
N
N而另一个是
H
,
t
H,t
H,t. 其中
N
N
N是信号的总长度，而
H
,
t
H,t
H,t是信号在t时刻后缀的长度(暂且这么理解，后面不对再改).
4 Open-loop Controller Synthesis
MILP（混合整数线性规划）中的约束分为系统约束与STL约束两部分，下面分别进行了介绍.
A. Constraints on system evolution
系统约束，即信号轨迹要满足系统转移函数
x
t
+
1
=
f
(
x
t
,
u
t
)
x_{t+1}=f(x_t,u_t)
xt+1=f(xt,ut).
B. STL constraints
引入了一个满足标志位
z
t
φ
z^\varphi_t
ztφ, 用来表示在
t
t
t时刻信号是否满足
φ
\varphi
φ. 那么可以推测，
z
φ
z^\varphi
zφ应该是一条与信号轨迹等长的序列，其值取0或1.
命题约束:
那么如何将命题针对优化问题进行编码呢？对于线性的原子命题
x
t
≥
μ
x_t \geq \mu
xt≥μ，定义
μ
(
x
t
)
=
x
t
−
μ
\mu(x_t)=x_t-\mu
μ(xt)=xt−μ，于是有：
μ
(
x
t
)
≤
M
t
z
t
μ
−
ϵ
t
−
μ
(
x
t
)
≤
M
t
(
1
−
z
t
μ
)
−
ϵ
t
\begin{aligned} \mu\left(x_{t}\right) & \leq M_{t} z_{t}^{\mu}-\epsilon_{t} \\ -\mu\left(x_{t}\right) & \leq M_{t}\left(1-z_{t}^{\mu}\right)-\epsilon_{t} \end{aligned}
μ(xt)−μ(xt)≤Mtztμ−ϵt≤Mt(1−ztμ)−ϵt
上式中
M
t
M_t
Mt是一个任意大的数，
ϵ
t
\epsilon_t
ϵt是一个任意小的数.
- 如果
t
t
t时刻的信号或信号后缀满足公式
μ
\mu
μ，则
z
t
μ
=
1
z_t^\mu=1
ztμ=1, 上式变为：
μ
(
x
t
)
≤
M
t
−
ϵ
t
−
μ
(
x
t
)
≤
−
ϵ
t
\begin{aligned} \mu\left(x_{t}\right) & \leq M_{t}-\epsilon_{t} \\ -\mu\left(x_{t}\right) & \leq -\epsilon_{t} \end{aligned}
μ(xt)−μ(xt)≤Mt−ϵt≤−ϵt
即
μ
(
x
t
)
>
0
\mu(x_t)\gt0
μ(xt)>0
- 如果不满足公式
μ
\mu
μ, 则
z
t
μ
=
0
z_t^\mu=0
ztμ=0, 上式变为：
μ
(
x
t
)
≤
−
ϵ
t
−
μ
(
x
t
)
≤
M
t
−
ϵ
t
\begin{aligned} \mu\left(x_{t}\right) & \leq -\epsilon_{t} \\ -\mu\left(x_{t}\right) & \leq M_{t}-\epsilon_{t} \end{aligned}
μ(xt)−μ(xt)≤−ϵt≤Mt−ϵt
即
μ
(
x
t
)
<
0
\mu(x_t)<0
μ(xt)<0
MILP变量的逻辑操作
这里定义可以对满足标志信号进行逻辑操作. 为什么需要操作这个信号呢？是为了后面递归地计算出
z
0
μ
z_0^\mu
z0μ
非:
z
t
ψ
=
¬
z
t
φ
z
t
ψ
=
1
−
z
t
φ
\text{非: } z_{t}^{\psi}=\neg z_{t}^{\varphi} \quad z_{t}^{\psi}=1-z_{t}^{\varphi}
非: ztψ=¬ztφztψ=1−ztφ
这一条比较好理解，如果信号满足命题
ψ
\psi
ψ，那么信号一定不满足
ψ
\psi
ψ的反命题。
与:
z
t
ψ
=
∧
i
=
1
m
z
t
i
φ
i
z
t
ψ
≤
z
t
i
φ
i
,
i
=
1
,
…
,
m
and
z
t
ψ
≥
1
−
∑
i
=
1
m
(
1
−
z
t
i
φ
i
)
\text{与: } z_{t}^{\psi}=\land_{i=1}^{m} z_{t_{i}}^{\varphi_{i}} \quad z_{t}^{\psi} \leq z_{t_{i}}^{\varphi_{i}}, i=1, \ldots, m \text{ and } z_t^\psi\geq1-\sum\limits_{i=1}^m(1-z^{\varphi_i}_{t_i})
与: ztψ=∧i=1mztiφiztψ≤ztiφi,i=1,…,m and ztψ≥1−i=1∑m(1−ztiφi)
定义这一步操作的目的是为了给下面的Always算子提供计算基础。
预计算
z
t
ψ
ψ
=
□
[
a
,
b
]
φ
∵
∀
t
i
∈
[
t
+
a
,
t
+
b
]
s
[
t
i
]
⊨
φ
∴
z
t
ψ
=
∧
i
=
1
m
z
t
i
φ
\text{预计算}z_t^{\psi}\ \ \psi=\square_{[a,b]}\varphi\\ \because \forall t_i \in[t+a,t+b] \ \ s[t_i]\models \varphi \\ \therefore z^\psi_t = \land^m_{i=1} z_{t_i}^{\varphi}
预计算ztψ ψ=□[a,b]φ∵∀ti∈[t+a,t+b] s[ti]⊨φ∴ztψ=∧i=1mztiφ
或操作同理：
或:
z
t
ψ
=
∨
i
=
1
m
z
t
i
φ
i
z
t
ψ
≥
z
t
i
φ
i
,
i
=
1
,
…
,
m
and
z
t
ψ
≤
∑
i
=
1
m
z
t
i
φ
i
\text{或: }z_{t}^{\psi}=\lor_{i=1}^{m} z_{t_{i}}^{\varphi_{i}} \quad z_{t}^{\psi} \geq z_{t_{i}}^{\varphi_{i}}, i=1, \ldots, m \text{ and } z_{t}^{\psi} \leq \sum\limits_{i=1}^{m} z_{t_{i}}^{\varphi_{i}}
或: ztψ=∨i=1mztiφiztψ≥ztiφi,i=1,…,m and ztψ≤i=1∑mztiφi
时序约束
包含时序操作子的公式所定义的约束成为时序约束，这里定义了
⋄
\diamond
⋄,
□
\square
□和
U
[
a
,
b
]
\mathcal{U}_{[a,b]}
U[a,b]三种时序操作子的编码方式。
Always:
ψ
=
□
[
a
,
b
]
φ
⇒
z
t
ψ
=
∧
i
=
min
(
t
+
a
,
N
)
min
(
t
+
b
,
N
)
z
i
φ
\psi=\square_{[a, b]} \varphi \quad \Rightarrow \quad z_{t}^{\psi}=\land_{i=\min (t+a, N)}^{\min (t+b, N)} z_{i}^{\varphi}
ψ=□[a,b]φ⇒ztψ=∧i=min(t+a,N)min(t+b,N)ziφ
Eventually:
ψ
=
⋄
[
a
,
b
]
φ
⇒
z
t
ψ
=
∨
i
=
min
(
t
+
a
,
N
)
min
(
t
+
b
,
N
)
z
i
φ
\psi=\diamond_{[a, b]} \varphi \quad \Rightarrow \quad z_{t}^{\psi}=\lor_{i=\min (t+a, N)}^{\min (t+b, N)} z_{i}^{\varphi}
ψ=⋄[a,b]φ⇒ztψ=∨i=min(t+a,N)min(t+b,N)ziφ
Until:
ψ
=
φ
1
U
[
a
,
b
]
φ
2
⇒
z
t
φ
1
U
[
a
,
b
]
φ
2
=
z
t
□
[
0
,
a
]
φ
1
∧
z
t
⋄
[
a
,
b
]
φ
2
∧
z
t
⋄
[
a
,
a
]
(
φ
1
U
φ
2
)
\psi=\varphi_{1} \mathcal{U}_{[a, b]} \varphi_{2} \quad \Rightarrow \quad z_t^{\varphi_1\ \mathcal{U}_{[a,b]}\varphi_2} = z_t^{\square_{[0,a]}\varphi_1}\land z_t^{\diamond_{[a,b]}\varphi_2}\land z_t^{\diamond_{[a,a]}(\varphi_1 \mathcal{U} \varphi_2)}
ψ=φ1U[a,b]φ2⇒ztφ1 U[a,b]φ2=zt□[0,a]φ1∧zt⋄[a,b]φ2∧zt⋄[a,a](φ1Uφ2)
编码的复杂度分析
由于总共
∣
P
∣
|P|
∣P∣个原子命题, 对应长度为N的信号, 因此产生满足标志信号z的数量为
O
(
N
⋅
∣
P
∣
)
O(N\cdot|P|)
O(N⋅∣P∣)。
优化问题中连续变量的数目是
O
(
N
⋅
∣
φ
∣
)
O(N\cdot|\varphi|)
O(N⋅∣φ∣),
∣
φ
∣
|\varphi|
∣φ∣是公式中操作子的数量。看了下一节才知道原来这个continuous variable指的是后面的鲁棒性信号。
5 Robustness-based Encoding
基于鲁棒性的编码方式是一种与上面不同的编码方式，这里把鲁棒性编码进目标函数
J
J
J里。
这里用定义了一个新的变量
r
t
φ
r^\varphi_t
rtφ，用来表示信号在
t
t
t时刻对于公式
φ
\varphi
φ的鲁棒性。那么优化问题的命题约束就简化为了
r
t
φ
>
0
r_t^\varphi \gt 0
rtφ>0。
接着又定义了一个新的二元变量
p
t
i
φ
i
p_{t_i}^{\varphi_i}
ptiφi…
算了我实在看不懂了，先看案例吧。
6 Model Predictive Control Synthesis
A. Synthesis for bounded-time STL formulas
B. Extension to unbounded formulas
7 Experimental Results
A. Boolean vs Robust Encoding
B. Mathematical Model of a Building
8 Discussion
未来工作
心得与记录
- 可能是我理解能力有限，我觉得这篇文章写得蛮凌乱的，每次看到一半看不下去，断断续续花了好几天才看完
