Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.03017 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915913002909696 |
|---|---|
| author | Capucci, Matteo Myers, David Jaz |
| author_facet | Capucci, Matteo Myers, David Jaz |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_03017 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Compositionality of Lyapunov functions via assume-guarantee reasoning Capucci, Matteo Myers, David Jaz Logic in Computer Science Category Theory Dynamical Systems 93D30, 68Q60, 18N10 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. |
| title | Compositionality of Lyapunov functions via assume-guarantee reasoning |
| topic | Logic in Computer Science Category Theory Dynamical Systems 93D30, 68Q60, 18N10 |
| url | https://arxiv.org/abs/2604.03017 |