Fossil 2.0：用于动力学模型验证与控制的形式化证书合成
系统与控制
2024-04-17 v2 机器学习
计算机科学中的逻辑
系统与控制
摘要
本文介绍 Fossil 2.0，这是一个用于为建模为常微分方程与差分方程的动力学系统合成证书（例如 Lyapunov 函数和 barrier 函数）的软件工具的新主要版本。Fossil 2.0 相较初始版本有大幅改进，包括新接口、显著扩展的证书组合、控制器合成以及增强的可扩展性。我们作为本工具论文的一部分展示这些新特性。Fossil 实现了反例引导的归纳合成（CEGIS）循环，以确保方法的可靠性。我们的工具使用神经网络作为模板来生成候选函数，随后由充当断言验证器的 SMT 求解器进行形式化证明。相较第一版的改进包括更广泛的证书范围、控制律的合成以及对离散时间模型的支持。
引用
@article{arxiv.2311.09793,
title = {Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models},
author = {Alec Edwards and Andrea Peruffo and Alessandro Abate},
journal= {arXiv preprint arXiv:2311.09793},
year = {2024}
}
备注
HSCC 2024 Tool Paper