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

Adnane Saoud; Alessio Iovine; Bart Besselink; Guillaume Sandou; Yoshinari Takayama

arxiv: 2605.04222 · v2 · pith:W36J7RO2new · submitted 2026-05-05 · 📡 eess.SY · cs.RO· cs.SY

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 This is my paper

Pith reviewed 2026-05-08 18:22 UTC · model grok-4.3

classification 📡 eess.SY cs.ROcs.SY

keywords layered control architecturesassume-guarantee contractssafety invarianceliveness refinementvertical refinementmodel predictive controlreference governorhybrid energy storage

0 comments

The pith

A heterogeneous contract framework enforces safety by invariance at the continuous layer and liveness by refinement at the discrete layer for layered control.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Real-world control systems must meet long-horizon objectives while respecting continuous-time safety constraints, which motivates hierarchical layered architectures. The paper addresses gaps in uniform specification, formal preservation across time scales, and compositional design by importing the safety-liveness split into an assume-guarantee contract. Safety holds because the continuous-time dynamics remain inside an invariant set, while liveness follows from refining discrete plans to satisfy the objectives. Layers coordinate through vertical refinement relations and timing-compatibility conditions that preserve both properties when subsystems connect. The approach is instantiated with a specific layered controller and tested on a hybrid energy storage system.

Core claim

Safety is enforced by invariance at the continuous-time layer, while liveness is achieved through refinement at the discrete-time layer, with inter-layer coordination formalized via vertical refinement and timing-compatibility conditions. This contract is instantiated by combining an MPC planner, an input-to-state stabilizing low-level controller, and a reference-governor bridge, and is validated on a Hybrid Energy Storage System comprising a battery and a supercapacitor.

What carries the argument

the heterogeneous assume-guarantee contract framework, which decomposes safety via continuous-time invariance from liveness via discrete-time refinement and coordinates layers via vertical refinement and timing-compatibility conditions

If this is right

A uniform specification language applies across discrete planning and continuous execution.
Formal guarantees are preserved when interconnecting subsystems operating at heterogeneous time scales.
Compositional separation between layers is achieved without reliance on naive input-filtering laws.
The framework supports co-design of an MPC planner with an input-to-state stabilizing controller and reference-governor bridge.
The instantiated controller satisfies both safety and liveness on a hybrid energy storage system with battery and supercapacitor.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Designers could attach new discrete planners to existing continuous safe controllers while retaining prior safety proofs if the refinement conditions hold.
The timing-compatibility rules might be verified through simulation for applications such as vehicle path planning with actuator dynamics.
If the conditions are met, the method could reduce the need for overly conservative safety buffers that limit performance in energy or motion systems.

Load-bearing premise

The vertical refinement and timing-compatibility conditions can be satisfied when interconnecting the MPC planner, ISS low-level controller, and reference-governor bridge without introducing new safety violations or performance loss.

What would settle it

A concrete counterexample in which a system satisfying the invariance, refinement, vertical refinement, and timing-compatibility conditions still violates a continuous-time safety constraint or fails to achieve a discrete liveness objective.

Figures

Figures reproduced from arXiv: 2605.04222 by Adnane Saoud, Alessio Iovine, Bart Besselink, Guillaume Sandou, Yoshinari Takayama.

**Figure 1.** Figure 1: Layered control architecture. Signals: rk (reference), yk (sampled state), v(t) (filtered reference), u(t) (control), x(t) (state), w(t) (disturbance). Signal flow: r → v → x. Section 4. This filtered reference v is a filtered version of the high-level system’s output r(t). The vector field f is locally Lipschitz in x, κ is locally Lipschitz, r(t) is piecewise constant, and w(t) ∈ W is piecewise continuou… view at source ↗

**Figure 2.** Figure 2: Vertical refinement for liveness specifications view at source ↗

**Figure 3.** Figure 3: Invariance in the augmented state space. The set K˜ = {(e, v) : V (e) ≤ Γ(v)} is a safe set in the augmented (e, v)-space, with barrier function Φ(e, v) := V (e)−Γ(v). For a fixed reference v, the slice Kv = {e : V (e) ≤ Γ(v)} (blue boundary) represents the allowable error states; this slice shrinks as v approaches constraint boundaries where Γ(v) decreases. The ISS ultimate bound Ωh = {e : V (e) ≤ V h} (b… view at source ↗

**Figure 4.** Figure 4: Hierarchical decomposition of tracking errors. The diagram illustrates the physical components of the Total Planner Deviation (Blue brace). This deviation aggregates the Governor Lag ∥v(t) − rk∥ (Green brace) and the Inner-Loop Control Error e(t) (Red brace). Note that while the continuous state Vgr(t) (Red line) may transiently violate the asymptotic tracking tube ±ε (Green shaded region), it settles b… view at source ↗

**Figure 5.** Figure 5: Hierarchical structure of the HESS dynamics. Output maps. The tracked output hr(x) = Pr x ∈ R 2 in Definition 1 selects the fast states that the low-level controller u = κ(x, v) as in (2) regulates the fast states (the currents, whose dynamics are not modeled in the high-level), i.e., hr(x) = Pr x = [Vgr, IB] ⊤, Pr ∈ R 2×5 . (81) The planner measurement yk = hy(x(tk)) ∈ R 2 in Definition 2 extracts the sl… view at source ↗

**Figure 6.** Figure 6: Phase portrait under mixed disturbance. The trajec view at source ↗

**Figure 7.** Figure 7: confirms that the ISS envelope (108) bounds ∥e(t)∥ at every instant, and that ∥e(t)∥ ≤ (1 + δ)ε = 3.02 V for all t ≥ τ2. The lower panel shows the hindsight computation of m(t), peaking at m = 2.94 during the initial transient. 0 1 2 3 4 5 Time [s] 0 2 4 6 8 |z(t)| [V] 2 |z(t)| ISS envelope (1+ ) view at source ↗

**Figure 8.** Figure 8: Scenario B: full hierarchical operation under time– view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

read the letter

The paper gives a contract framework that separates continuous-time safety via invariance from discrete-time liveness via refinement, coordinated by vertical refinement and timing conditions, and shows it on an MPC-ISS-governor HESS example. It fills the three gaps it identifies in layered control work: a uniform language across layers, preservation of specs when time scales differ, and real compositional separation instead of ad-hoc filtering. The concrete instantiation with an MPC planner, an ISS low-level controller, and a reference-governor bridge on a battery-supercapacitor plant makes the claims testable and shows how the coordination rules can be checked in practice. That part is useful because many real systems mix slow planning with fast execution and need both long-horizon goals and hard safety bounds. The example appears to satisfy the timing-compatibility and vertical refinement conditions without obvious contradictions on the reported dynamics. The math imports standard assume-guarantee and invariance ideas but applies them in a heterogeneous vertical setting, which is the actual new piece. One soft spot is the reference-governor bridge itself. It must transmit the continuous invariance set while respecting the ISS gain and the MPC horizon; if the paper only validates this on one set of HESS parameters without explicit computation of the composed invariant or checks for cases where the governor shrinks the safe set, then the preservation claim rests on that specific case rather than a general argument. The stress-test concern about new violations or liveness loss is reasonable to raise, though the abstract suggests the authors believe the conditions hold for their plant. Readers working on formal control of hybrid or hierarchical systems in robotics or energy storage will get the most from it. The structure is clear enough and the application concrete enough that it deserves a serious referee to check the derivations and the example in detail. I would send it to peer review.

Referee Report

1 major / 0 minor

Summary. The manuscript proposes a heterogeneous assume-guarantee contract framework for layered control architectures (LCAs). Safety is enforced by invariance at the continuous-time layer while liveness is achieved through refinement at the discrete-time layer, with inter-layer coordination formalized via vertical refinement and timing-compatibility conditions. The framework is instantiated with an MPC planner, an input-to-state stabilizing (ISS) low-level controller, and a reference-governor bridge, and validated on a hybrid energy storage system (HESS) comprising a battery and supercapacitor.

Significance. If the vertical refinement and timing-compatibility conditions hold for the instantiation, the work would advance the field by supplying a uniform specification language and compositional guarantees for safety-liveness decomposition across heterogeneous time scales in LCAs. The explicit separation of concerns, the concrete MPC-ISS-governor architecture, and the HESS case study address documented gaps in existing layered control research and could support modular co-design in safety-critical applications.

major comments (1)

The central claim requires that the assume-guarantee contracts compose via vertical refinement and timing-compatibility conditions so that continuous-time invariance (safety) is preserved under discrete-time refinement (liveness) for the MPC + ISS + reference-governor instantiation. However, no explicit computation of the composed invariant or verification that the governor's filtering law transmits the invariance set without shrinkage (while satisfying the ISS gain and MPC horizon timing) is supplied for the reported HESS dynamics; this is load-bearing for the safety guarantee.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment of the work's significance and for the constructive major comment. We address it directly below and will revise the manuscript to strengthen the explicit safety verification.

read point-by-point responses

Referee: The central claim requires that the assume-guarantee contracts compose via vertical refinement and timing-compatibility conditions so that continuous-time invariance (safety) is preserved under discrete-time refinement (liveness) for the MPC + ISS + reference-governor instantiation. However, no explicit computation of the composed invariant or verification that the governor's filtering law transmits the invariance set without shrinkage (while satisfying the ISS gain and MPC horizon timing) is supplied for the reported HESS dynamics; this is load-bearing for the safety guarantee.

Authors: We agree that an explicit computation of the composed invariant for the HESS dynamics, together with verification that the reference governor's filtering law transmits the invariance set without shrinkage while respecting the ISS gain and MPC horizon timing, would make the safety guarantee fully concrete and load-bearing. The manuscript derives the general vertical refinement and timing-compatibility conditions that guarantee invariance preservation by construction for any system satisfying the MPC-ISS-governor assumptions, and it proves these conditions hold abstractly for the architecture. The HESS example demonstrates the overall layered control realization but does not include the numerical invariant computation or governor-specific verification for the reported battery-supercapacitor dynamics. In the revised manuscript we will add this computation, explicitly constructing the invariant set for the HESS model and confirming transmission without shrinkage under the chosen ISS gain and MPC timing parameters. revision: yes

Circularity Check

0 steps flagged

Standard safety-liveness decomposition imported into heterogeneous contracts with independent coordination conditions

full rationale

The derivation imports the known safety-by-invariance / liveness-by-refinement split and assume-guarantee contracts, then adds vertical refinement and timing-compatibility conditions defined directly in the paper. No equation reduces to a fitted parameter renamed as a prediction, no self-definition of the target result, and no load-bearing uniqueness theorem imported solely from the authors' prior work. The central claim (composition preserves invariance and refinement for the MPC+ISS+governor instantiation) is an application rather than a tautology; any self-citations are non-load-bearing background. This yields a normal low circularity score.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The framework rests on standard domain assumptions from control theory and contract-based design while introducing a new coordination entity; no free parameters are mentioned in the abstract.

axioms (2)

domain assumption Safety can be enforced by set invariance in continuous-time dynamical systems
Invoked as the mechanism for the continuous-time safety layer.
domain assumption Liveness properties can be achieved through successive refinement in discrete-time planning layers
Invoked as the mechanism for the discrete-time liveness layer.

invented entities (1)

Reference-governor bridge no independent evidence
purpose: To enforce vertical refinement and timing-compatibility between the MPC planner and ISS low-level controller
Introduced as the inter-layer coordinator in the concrete instantiation.

pith-pipeline@v0.9.0 · 5512 in / 1467 out tokens · 57887 ms · 2026-05-08T18:22:58.075753+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

Foundation/ArrowOfTime, Cost.FunctionalEquation No parallel — quadratic Lyapunov / linear ISS, not the cosh-cost J(x) = ½(x+x⁻¹)−1 forced by washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

ISS-Lyapunov function V(e)=e^T P e ... ¯V_h(H_max) := ᾱ(α^{-1}(σ(H_max)))
Constants (zero-parameter ladder) Tunable design parameters, antithetical to RS's parameter-free derivation of c, ℏ, G as φ-powers unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

controller gains k₁ = 25 s⁻², k₂ = 11 s¹ ... Q = diag(50,1) ... sampling period Tₛ

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.