用于观测自主系统序列类行为的静态测试环境综合

本文研究面向自主系统高层任务目标（特别是可达性）的形式化测试用例生成。我们使用Kripke结构表示被测智能体的高层决策以及测试环境的抽象。首先，我们定义测试规范的概念，重点关注由序列时序逻辑公式表示的一段线性时序逻辑。其次，我们形式化测试图综合问题，以寻找一种测试配置，使得智能体必须满足测试规范才能满足其任务目标。我们提出一种基于网络流的算法，通过对由Kripke结构诱导的原始图上的转移（以边删除表示）进行限制来综合测试图。该算法利用整数线性规划迭代地综合测试图。我们证明了算法的完备性，并表明每次迭代中的边删除保持了后续迭代中整数线性规划的可行性。我们根据最大流形式化最小约束测试图的概念，并证明所综合的测试图是最小约束的。我们在简单图和网格世界上演示了我们的算法。