又是一篇有关STL任务分解的文章
[1] Z. Zhang and S. Haesaert, “Modularized Control Synthesis for Complex Signal Temporal Logic Specifications.” arXiv, Mar. 29, 2023. doi: 10.48550/arXiv.2303.17086.
Outline
- 通过一系列规则将复杂的STL公式转化为独立的模块，从而提高MILP的求解效率
- 证明了分解后子公式与原公式的等价性
- 提出LSR方法求解控制律
1 Intro
通常的STL综合问题使用MILP进行编码求解，但是当公式比较复杂的时候求解时间很长，因此本文提出使用模块化公式的方法，分开求解控制律以提升计算效率。
提升控制综合效率的方法还有：
- model checking方法：[14]将STL转化为timed Automata
- CBF[12]和Funnel法[15]
2 Preliminaries and Problem Statement
系统表示
本文处理连续时间系统，系统动态由以下微分方程表示：
STL语法分解
定义子公式：不可用布尔逻辑算子继续分解的公式
分解规则：
φ
=
φ
1
U
(
a
,
b
)
φ
2
\varphi=\varphi_1 U_{(a,b)}\varphi_2
φ=φ1U(a,b)φ2能够拆分为(4)式
- (4)式在说什么呢？
-
φ
=
φ
1
U
(
a
,
b
)
φ
2
\varphi=\varphi_1 U_{(a,b)}\varphi_2
φ=φ1U(a,b)φ2能够以两种情况成立，这里以递归的形式进行定义
- 要么在某个
τ
\tau
τ时刻之前完成
- 如果在
τ
\tau
τ时刻之后完成，则
(
a
,
τ
)
(a,\tau)
(a,τ)时
φ
1
\varphi_1
φ1一直成立，并且在
τ
\tau
τ瞬间，再次分两种情况：
-
φ
1
\varphi_1
φ1和
φ
2
\varphi_2
φ2在这一瞬间同时成立
- 或者之后剩下的时间里满足
φ
1
U
(
0
,
b
−
t
)
φ
2
\varphi_1 U_{(0,b-t)}\varphi_2
φ1U(0,b−t)φ2
- 简单的来说，就是对于
(
a
,
b
)
(a,b)
(a,b)中的任何一个时刻
τ
\tau
τ，要么在这个时间前、要么当时、要么之后确定公式的满足性
- 这里的花括号
{
τ
}
\{\tau\}
{τ}表示
t
=
τ
t=\tau
t=τ这个时间点
Reachable Set and Largest Satisfaction Region
接下来要我们一步一步引入本文最核心的概念——LSR
-
R
τ
(
X
0
)
\mathscr R_\tau(\mathscr X _0)
Rτ(X0)reachable set: 由某一初始状态集合出发在**
τ
\tau
τ时刻的所有可能状态**
-
R
τ
−
1
(
X
τ
)
\mathscr R_\tau^{-1}(\mathscr X _\tau)
Rτ−1(Xτ) inverse reachable set: 能到达当前状态的全部初始状态
-
U
τ
(
X
0
,
φ
)
\mathscr U_\tau(\mathscr X _0,\varphi)
Uτ(X0,φ) admissible control set: 所有使得系统状态不违反约束的的控制序列
-
S
0
(
φ
)
S_0(\varphi)
S0(φ) largest specification region: 存在控制下最大的初始状态集合，使得轨迹满足约束（也就是排除掉怎么都会破坏约束的剩余初始状态）
Problem Statement
本文接下来要解决三个问题：
-
分解STL公式，使得时间区间尽量短且没有区域重合
-
由子公式的LSR得到原公式的LSR
-
从LSR中选择一个初始状态设计开环控制器
3 Main Results
这一章中，首先定义了什么是充分分解式，其次提出了一套将普通公式转化为这类公式的方法，最后提出使用模块化方法求解LSR与控制律
A. Sufficiently Separate Formulas
- S2-formulas: 子公式的时间区间不重合的公式
- 以下两种公式的所有的子公式没有重合的时间内区间为充分分离
-
γ
\gamma
γ-formulas: always式的逻辑与组合
-
ξ
\xi
ξ-formulas: eventually式的逻辑或组合
-
γ
\gamma
γ型和
ξ
\xi
ξ型公式的数量相等称为充分分离
-
ψ
\psi
ψ-formula: 上面2种公式的逻辑与组合
B. 将
ψ
\psi
ψ型公式转化为
S
2
S^2
S2型
首先看两条引理：
Lemma 1:
- 对于单个时间点，always和eventually等价
- 对于单个时间点，always or可以直接拆分（一般情况是不能的）
- 对于单个时间点，always always和eventually eventually可以直接简化
Lemma 2:
- always可以用and将时间区间拆开，eventually可以用or将时间区间拆开
分别可以对
γ
\gamma
γ型和
ξ
\xi
ξ型公式引出分解规则：
- 时间区间的拆分
- 布尔逻辑的拆分
以上的拆分方法都是不改变语义的，能够保证公式的soundness
C.Modularized Solution of Largest Satisfying Regions
B中的方法能够将所有的
ψ
\psi
ψ型公式转化为S2型，这一部分介绍了如何从子公式的LSR中求解复杂总公式的LSR。
τ
\tau
τ-LSR
- 前面的LSR
S
0
S_0
S0 为初始状态集合，而Def4修改定义为
τ
\tau
τ时刻状态集合
- 总公式的LSR根据子公式的布尔逻辑组合方式得到（显而易见）
D. Modularized Synthesis of an
Ψ
\Psi
Ψ-class formula
控制综合3步走：
- 将
ψ
\psi
ψ型公式分解为
γ
\gamma
γ型和
ξ
\xi
ξ型公式两类
- 求解每个子公式的LSR，并利用C中的规则得到总LSR
- 模块化控制综合
- 第
j
j
j个公式头部第与
j
j
j个公式尾部的定义:
- 由于分解过程中涉及到时间区间的分割，因此需要确保轨迹的连贯性：设计控制器时需保证
a
j
+
1
a_{j+1}
aj+1时刻的状态落在剩余公式的LSR中
- 这个方法提升效率的原因在于每当过去的一个子公式被满足，就可以以后不用再考虑
- 对于eventually子公式有一个特殊处理，不需要等到子公式的时域结束就能够判断其满足性，因此只要为真就移除，以减小计算负担
- 通过求解优化问题得到问题的解
4 Case Study
实验场景设置为如下平面空间，机器人考虑为单积分器模型，控制量大小有上限。
机器人要处理的任务为：
ψ
=
G
[
0
,
30
]
φ
0
∧
G
[
15
,
45
]
φ
1
∧
F
[
0
,
45
]
φ
2
\psi=G_{[0,30]}\varphi_0 \land G_{[15,45]}\varphi_1 \land F_{[0,45]}\varphi_2
ψ=G[0,30]φ0∧G[15,45]φ1∧F[0,45]φ2
- 30秒前，每5秒至少访问一次
Z
0
Z_0
Z0:
φ
0
=
F
[
0
,
5
]
(
ζ
∈
Z
0
)
\varphi_0=F_{[0,5]}(\zeta\in Z_0)
φ0=F[0,5](ζ∈Z0)
- 15s-45s，机器人离开
Z
1
Z_1
Z1后必须在5s内回来 : 6
φ
1
=
¬
(
ζ
∈
Z
1
)
→
F
[
0
,
5
]
(
ζ
∈
Z
1
)
\varphi_1=\neg(\zeta\in Z_1)\to F_{[0,5]}(\zeta\in Z_1)
φ1=¬(ζ∈Z1)→F[0,5](ζ∈Z1)
- 45s前，必须在
Z
2
Z_2
Z2内待够3s充电 :
G
[
0
,
3
]
(
ζ
∈
Z
2
)
G_{[0,3]}(\zeta\in Z_2)
G[0,3](ζ∈Z2)
接下来作者用这个例子一步一步演示了自己的算法：
第一步：将原公式改写为S2型
第二步：求LSR，也就是Fig 1中粉红色的部分
第三步：模块化控制综合
根据第一步的分解，将公式切分为了0-15,15-30和30-45三段，因此分段求出了控制律
得到的轨迹信息如下，可见总轨迹是满足STL约束的，且求解优化问题的总时间明显更短
5 Conclusion
局限：
- 只处理always和eventually的分解
- 开环，对不确定性不具有鲁棒性
读后心得
- 所谓模块化，不如说是分阶段求解，本文实际上上将复杂公式拆解为时间窗口不重合几段进行分别求解
