安全关键自主系统控制器的形式化综合：进展与挑战
系统与控制
2024-02-21 v1 机器人学
系统与控制
摘要
近年来，形式化方法已广泛用于自主系统的设计。通过采用数学上严谨的技术，形式化方法可以为具有连续动力学与离散逻辑之间复杂交互的复杂动态系统提供具有可证明安全保证的全自动推理过程。本文全面回顾了安全关键自主系统的形式化控制器综合技术。具体而言，我们根据不同的系统模型（包括确定性、非确定性和随机性）以及涉及逻辑、实时和实值域的各种形式化安全关键规范，对形式化控制综合问题进行了分类。该综述涵盖了基本的形式化控制综合技术，包括基于抽象的方法和免抽象的方法。我们探讨了数据驱动综合方法在形式化控制综合中的集成。此外，我们回顾了专为多智能体系统 (MAS) 定制的形式化技术，特别关注解决大规模系统可扩展性挑战的各种方法。最后，我们讨论了一些最新趋势并强调了该领域的研究挑战。
引用
@article{arxiv.2402.13075,
title = {Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges},
author = {Xiang Yin and Bingzhao Gao and Xiao Yu},
journal= {arXiv preprint arXiv:2402.13075},
year = {2024}
}