基于假设-保证推理的 Lyapunov 函数的组合性

假设-保证推理是一种组合化模型检验技术，其中在系统参数或输入的某些假设下检验系统规范，并对系统状态的观测提供保证。我们通过将系统视为透镜（lenses），提出了一个用于安全问题的假设-保证推理的范畴框架，延续了我们关于广义 Moore 机器组合性的早期工作。广义 Moore 机器包括普通 Moore 机器、部分可观测马尔可夫（决策）过程以及参数化 ODE（控制系统）系统；我们的框架为每种情况专门提供了假设-保证推理。特别地，我们给出了参数化 ODE 系统上（局部）输入到状态稳定性（(L)ISS）Lyapunov 函数的假设-保证推理的新表述。我们的框架在范畴意义上是自然的且直接具有组合性。广义 Moore 机器的一种类型由切性（tangency）决定：带有截面的纤维化。我们证明了在切性 2-范畴内部的纤维化可以从认证连线图的对称单子宽松右模 2-函子地构造出对称单子双范畴上的认证广义 Moore 机器的假设-保证模块。