Search papers, labs, and topics across Lattice.
This paper introduces a heterogeneous assume-guarantee contract framework for layered control architectures (LCAs) that decomposes safety as invariance at the continuous-time layer and liveness as refinement at the discrete-time layer. It addresses the lack of uniform specification languages, formal guarantees for interconnecting subsystems, and compositional separation between layers in existing LCA research. The framework is instantiated with an MPC planner, ISS controller, and reference-governor bridge, and validated on a Hybrid Energy Storage System.
Guaranteeing safety and liveness in complex control systems doesn't require monolithic design; this work shows how to decompose the problem across layers with formal contracts.
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.
