Compositionality of Lyapunov functions via assume-guarantee reasoning
This work addresses safety verification for complex systems like control systems and Markov processes, but it appears incremental as it builds on earlier categorical work on generalized Moore machines.
The paper tackles the problem of compositional safety verification for systems like control systems and Markov processes by developing a categorical framework for assume-guarantee reasoning, resulting in a novel formulation for Lyapunov functions in parameterized ODEs that is categorically natural and compositional.
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.