Safety by Invariance, Liveness through Refinement: Heterogeneous Contract Framework for Co-Design of Layered Control
For control systems engineers designing safety-critical layered controllers, this work provides a formal method to ensure both long-horizon objectives and continuous-time safety with compositional guarantees, addressing a key gap in existing LCA research.
The paper addresses the lack of a uniform specification language and formal compositional guarantees in hierarchical layered control architectures by introducing a heterogeneous assume-guarantee framework that decomposes safety (via invariance at continuous-time layer) and liveness (via refinement at discrete-time layer). The framework is validated on a Hybrid Energy Storage System, demonstrating formal preservation of specifications across layers.
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.