基于形式化验证的Lyapunov函数综合
系统与控制
2021-12-06 v1 系统与控制
摘要
近期在Lyapunov函数综合中采用SMT求解器，为自动构造Lyapunov函数及可靠的计算机辅助证书提供了有效工具。所提方法的主要益处在于形式正确性与数值不确定性的消除。本工作中，我们扩展了基于SMT的综合方法以适用于更广泛的连续与离散时间系统类别。此外，我们处理了状态依赖切换系统的Lyapunov函数构造问题。我们通过控制系统的文献中的多个实例阐释了我们的方法。
关键词
引用
@article{arxiv.2112.01835,
title = {Synthesis of Lyapunov Functions using Formal Verification},
author = {Lukas Munser and Grigory Devadze and Stefan Streif},
journal= {arXiv preprint arXiv:2112.01835},
year = {2021}
}