Reference. Compositionality of Lyapunov functions via assume-guarantee reasoning

Matteo Capucci, David Jaz Myers · arXiv · 2026 · dynamical-systems · DOI · arXiv
Assume-guarantee reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and provide guarantees on observations of system state. We present a categorical framework for assume-guarantee reasoning for safety problems by viewing systems as lenses, following our earlier work on the compositionality of generalized Moore machines. Generalized Moore machines include ordinary Moore machines, partially observable Markov (decision) processes, and systems of parameterized ODEs (control systems); our framework gives assume-guarantee reasoning specially adapted to each of these cases. In particular, we give a novel formulation of assume-guarantee reasoning for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs. Our framework is categorically natural and straightforwardly compositional. A flavor of generalized Moore machine is determined by a tangency: a fibration with a section. We show that symmetric monoidal loose right modules of assume-guarantee certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams can be constructed 2-functorially from fibrations internal to the 2-category of tangencies.

Cite
Cite as @capucci-2026-compositionality (helia, typst) · \cite{capucci-2026-compositionality} (LaTeX)
BibTeX
bibtex · 10 lines
@misc{capucci-2026-compositionality,
  doi = {10.48550/ARXIV.2604.03017},
  url = {https://arxiv.org/abs/2604.03017},
  author = {Capucci, Matteo and Myers, David Jaz},
  keywords = {Logic in Computer Science (cs.LO), Category Theory (math.CT), Dynamical Systems (math.DS), FOS: Computer and information sciences, FOS: Computer and information sciences, FOS: Mathematics, FOS: Mathematics, 93D30, 68Q60, 18N10},
  title = {Compositionality of Lyapunov functions via assume-guarantee reasoning},
  publisher = {arXiv},
  year = {2026},
  copyright = {arXiv.org perpetual, non-exclusive license}
}
hayagriva YAML (typst)
yaml · 11 lines
capucci-2026-compositionality:
  type: misc
  title: Compositionality of Lyapunov functions via assume-guarantee reasoning
  author:
  - Capucci, Matteo
  - Myers, David Jaz
  date: 2026
  publisher: arXiv
  url: https://arxiv.org/abs/2604.03017
  serial-number:
    doi: 10.48550/ARXIV.2604.03017
Download: capucci-2026-compositionality.bib · capucci-2026-compositionality.yml
Cites 36 works (2 here)
With notes (2)

Categorical Lyapunov Theory II: Stability of Systems ames-2025-categoricalarXiv · 2025
Lyapunov’s theorem provides a foundational characterization of stable equilibrium points in dynamical systems. In this paper, we develop a framework for stability for F-coalgebras. We give two definitions for a categorical setting in which we can study the stability of a coalgebra for an endofunctor F. One is minimal and better suited for concrete settings, while the other is more intricate and provides a richer theory. We prove a Lyapunov theorem for both notions of setting for stability, and a converse Lyapunov theorem for the second.
arXiv

Categorical Lyapunov Theory I: Stability of Flows ames-2025-categoricalxarXiv · 2025
Lyapunov’s theorem provides a fundamental characterization of the stability of dynamical systems. This paper presents a categorical framework for Lyapunov theory, generalizing stability analysis with Lyapunov functions categorically. Core to our approach is the set of axioms underlying a setting for stability, which give the necessary ingredients for “doing Lyapunov theory” in a category of interest. With these minimal assumptions, we define the stability of equilibria, formulate Lyapunov morphisms, and demonstrate that the existence of Lyapunov morphisms is necessary and sufficient for establishing the stability of flows. To illustrate these constructions, we show how classical notions of stability, e.g., for continuous and discrete time dynamical systems, are captured by this categorical framework for Lyapunov theory. Finally, to demonstrate the extensibility of our framework, we illustrate how enriched categories, e.g., Lawvere metric spaces, yield settings for stability enabling one to “do Lyapunov theory” in enriched categories.
arXiv
External (34)
capucci-2026-compositionality reference entries/refs/capucci-2026-compositionality/capucci-2026-compositionality.hel