Safety by Invariance, Liveness through Refinement: Heterogeneous Contract Framework for Co-Design of Layered Control
通过不变性保证安全,通过精化实现活性:分层控制协同设计的异构契约框架
Yoshinari Takayama, Alessio Iovine, Bart Besselink, Guillaume Sandou, Adnane Saoud
AI总结 针对分层控制架构缺乏统一规范语言、跨时间尺度互联保证及层间组合分离的问题,提出将安全-活性分解引入异构假设-保证契约框架,通过连续时间层的不变性保证安全,离散时间层的精化实现活性,并形式化层间协调条件。
详情
- Comments
- 21 pages
现实世界的控制系统必须在满足连续时间安全约束的同时实现长期目标(活性),这一组合推动了分层控制架构(LCA)的研究。然而,现有的LCA研究缺乏(i)跨离散规划和连续执行的统一规范语言,(ii)在异构时间尺度下互连子系统时保证规范得以保持的形式化保证,以及(iii)由于依赖简单的输入滤波法则而导致的层间组合分离。本文通过将安全-活性分解引入异构假设-保证框架来填补这三个空白:\emph{安全通过连续时间层的不变性}来保证,而\emph{活性通过离散时间层的精化}来实现,层间协调通过垂直精化和时间兼容性条件形式化。我们通过一个结合MPC规划器、输入到状态稳定(ISS)底层控制器和参考调节器桥的新型LCA实例化该契约,并在包含电池和超级电容器的混合储能系统(HESS)上进行了验证。
Real-world control systems must achieve long-horizon objectives (liveness) while respecting continuous-time safety constraints, a combination that motivates hierarchical layered control architectures (LCAs). Existing LCA research, however, lacks (i) a uniform specification language across discrete planning and continuous execution, (ii) formal guarantees that specifications are preserved when interconnecting subsystems at heterogeneous time scales, and (iii) compositional separation between layers, owing to reliance on naive input-filtering laws. This paper addresses all three gaps by importing the safety--liveness decomposition into a heterogeneous assume--guarantee framework: \emph{safety is enforced by invariance} at the continuous-time layer, while \emph{liveness is achieved through refinement} at the discrete-time layer, with inter-layer coordination formalized via vertical refinement and timing-compatibility conditions. We instantiate this contract with a novel LCA combining an MPC planner, an input-to-state stabilizing (ISS) low-level controller, and a reference-governor bridge, and validate it on a Hybrid Energy Storage System (HESS) comprising a battery and a supercapacitor.