论文标题
使用SMT求解器的Lyapunov函数的自动化和声音合成
Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
论文作者
论文摘要
在本文中，我们采用SMT求解器来综合主张给定动力学模型稳定性的Lyapunov函数。搜索lyapunov函数的构架是二阶逻辑公式的满意度，询问是否存在满足所需规范（稳定性）的函数，以适用于模型的所有可能初始条件。我们合成Lyapunov的线性，非线性（多项式）和参数模型的功能。对于非线性模型，该算法还确定了Lyapunov函数的有效性区域。我们从参数模板开始利用一个归纳框架来合成Lyapunov函数。归纳框架包括两个要素：学习者提出了lyapunov功能，验证者检查其有效性 - 其缺乏通过反例（在状态空间上的点）表示，以供学习者进一步使用。尽管验证者使用SMT求解器Z3，从而确保了过程的整体声音，但我们检查了学习者的两个替代方案：基于优化工具Gurobi的数值方法，以及再次基于Z3的声音方法。整体技术是通过广泛的基准进行评估的，这表明该方法不仅在合理的计算时间内缩放到10维模型，而且还为生成的Lyapunov函数及其有效性领域提供了新颖的合理性证明。
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as the satisfiability of a second-order logical formula, asking whether there exists a function satisfying a desired specification (stability) for all possible initial conditions of the model. We synthesise Lyapunov functions for linear, non-linear (polynomial), and for parametric models. For non-linear models, the algorithm also determines a region of validity for the Lyapunov function. We exploit an inductive framework to synthesise Lyapunov functions, starting from parametric templates. The inductive framework comprises two elements: a learner proposes a Lyapunov function, and a verifier checks its validity - its lack is expressed via a counterexample (a point over the state space), for further use by the learner. Whilst the verifier uses the SMT solver Z3, thus ensuring the overall soundness of the procedure, we examine two alternatives for the learner: a numerical approach based on the optimisation tool Gurobi, and a sound approach based again on Z3. The overall technique is evaluated over a broad set of benchmarks, which shows that this methodology not only scales to 10-dimensional models within reasonable computational time, but also offers a novel soundness proof for the generated Lyapunov functions and their domains of validity.
