Safety by Invariance, Liveness through Refinement: Heterogeneous Contract Framework for Co-Design of Layered Control

TL;DR

This paper proposes a formal, layered control framework combining safety invariance and liveness refinement, validated on a hybrid energy storage system, addressing key gaps in hierarchical control architectures.

Contribution

It introduces a heterogeneous assume-guarantee framework for layered control, ensuring safety and liveness with formal guarantees and compositional separation.

Findings

Validated on a Hybrid Energy Storage System with battery and supercapacitor.

Formal guarantees for safety preservation and liveness achievement.

A novel layered control architecture combining MPC, ISS controller, and reference-governor.

Abstract

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.