无限状态安全盾的不可实现性解释
计算机科学中的逻辑
2025-08-01 v1
摘要
安全强化学习致力于在确保安全的前提下开发最优策略。盾牌合成是一种流行方法，从逻辑规范中合成正确构造的安全组件。最近，盾牌合成已扩展到无限状态域，如连续环境。这使得盾牌更适用于现实场景。然而，规范可能因不一致（例如矛盾）而导致盾牌不可实现。在为此差距提供解决方案方面，我们提出了一种获取简单无条件和条件解释的方法，这些解释见证不可实现性，通过时序公式展开。在本文中，我们展示了该技术的不同变体及其适用性。
引用
@article{arxiv.2507.23603,
title = {Explanations for Unrealizability of Infinite-State Safety Shields},
author = {Andoni Rodriguez and Irfansha Shaik and Davide Corsi and Roy Fox and Cesar Sanchez},
journal= {arXiv preprint arXiv:2507.23603},
year = {2025}
}