使用基于混合 zonotope 的可达性分析对线性时序逻辑规范进行形式化验证

在本文中，我们引入了一种基于混合 zonotope 的方法，用于形式化验证在 Linear Temporal Logic（LTL）规范下运行的自主系统的行为。特别是，我们通过向后可达性分析（BRA）构建时序逻辑树（TLT）来形式化验证 LTL 公式。在以前的工作中，TLT 主要通过高度通用且计算量大的基于水平集的 BRA，或者简单且计算高效的基于多面体的 BRA 来构建。在这项工作中，我们转而提出使用基于混合 zonotope 的 BRA 来构建 TLT。通过使用混合 zonotope，我们表明我们能够以计算高效的方式形式化验证 LTL 规范，同时仍能表示在部署自主系统时经常出现的复杂几何形状，如非凸、不相交的集合。此外，我们在一个停车示例上评估了我们的方法，初步表明了混合 zonotope 如何在自然导致非凸、不相交几何形状的环境中促进 LTL 规范的计算高效形式化验证。