Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification
本文介绍了 Predictive Varanus，这是一个结合了基于 CSP 的一致性监控与预测性 LTL 分析的两阶段运行时验证流水线，通过利用现有的设计时模型，实现对自主系统中安全违规行为的更早期检测。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
从探索火星的漫游车到递送包裹的无人机，自主机器人运行在一个永远无法完全预测的世界中。即使是设计得最精密的机器，也可能遇到传感器故障、意外障碍物或工程师从未想象过的状况。为了保持这些系统的安全，科学家们使用了一种被称为运行时验证（runtime verification）的技术。可以将它想象成一个警觉的副驾驶，实时观察机器人的每一个动作，并根据任务开始前编写的一套规则来检查其行为。如果机器人试图做出被禁止的行为，副驾驶就会发出警报。然而，这种传统方法有一个致命缺陷：它是响应式的。它只有在错误已经发生后才会发出警报。在核设施或深空探测任务等高风险环境中，等待错误发生后再做出反应可能为时已晚。研究人员的目标是构建一个不仅能监测错误，而且能预见错误的系统，在机器人迈出导致失败的第一步之前就预测到失败。
这正是由一组研究人员解决的挑战，他们开发了一种名为 Predictive Varanus 的新型监控系统。该系统专为自主机器人设计，并在一个负责检查核废料储存库的模拟漫游车上进行了测试。研究人员结合了两种现有技术，创建了一个既严格限制机器人允许行为，又足够聪明以预见下一步走向的流水线。系统的第一部分充当“守门员”。它使用一种被称为通信顺序进程（Communicating Sequential Processes）的形式化语言，通过一份详细的机器人预期行为图谱来检查机器人执行 way 的每一个事件。如果机器人试图前往不该访问的位置，或者忽略了安全指令，守门员会立即拒绝该行为，将其判定为无效。这确保了机器人始终在设计的边界内运行。
系统的第二部分则是进行预测的地方。一旦守门员确认机器人的当前行为有效，系统就会向前展望。它提出了一个简单而强大的问题：鉴于机器人目前表现正常，它未来可能采取的唯一路径有哪些？通过分析机器人设计图谱中剩余的路径，系统可以确定某个特定结果是否已变得不可避免。它并不是在随机猜测可能性，而仅仅考虑与机器人自身规则一致的未来。如果机器人遇到了高辐射水平，系统便知道，唯一的允许路径是返回并中止任务。因此，甚至在机器人实际转身之前，系统就能确定地预测任务将会失败。同样，如果机器人已成功访问了所有要求的检查点，系统可以预测任务将会成功，即便机器人距离正式停止运行还有几个步骤。
研究人员在他们的核检查漫游车上测试了这种方法，该漫挪车被编程为访问五个不同的航标点并检查辐射水平。辐射水平被分为绿色、橙色和红色。如果漫游车看到橙色或红色，规则规定它必须返回起点并中止任务。在标准监控中，系统只有在漫游车实际返回后才会知道任务注定失败。而在使用 Predictive Varanus 的情况下，系统可以在漫游车甚至还没开始返回行程的两个事件之前，就宣布任务失败。在其他场景中，它可以在漫游车完成最后任务前八个事件之前，预测到成功的完成。这种早期预警为人类操作员或机器人自身的控制软件提供了宝贵的反应时间，例如重新规划路线或准备安全关机，而不是仅仅眼睁睁地看着失败发生。
该研究还测量了增加这一层思考过程所需的计算能力。守门员部分保持了极高的速度，即使在机器人的行为图谱变大时，每个事件的处理时间也低于一毫秒。预测部分负责执行“向前看”的任务，这需要耗费更多时间，尤其是当机器人的可能行为变得更加复杂时。对于一个拥有 200 个不同状态的模型，预测检查每次事件大约耗时 700 毫秒。虽然这变慢了，但研究人员发现，在许多情况下，提前获知结果所带来的收益足以抵消其成本。该系统成功识别了在机器人仍遵循规则时的必然失败和必然成功，证明了在不破坏现状逻辑的前提下，实现对未来的预判是可行的。
这项工作的意义不仅在于它能预测未来，更在于它如何实现预测。它并不依赖于一个独立的、抽象的预测模型。相反，它复用了最初用于验证机器人行为的完全相同的设计图谱。这意味着系统并非在对机器人的行为做假设，而是严格遵循工程师预先构建在机器中的逻辑。研究人员表明，通过将严格的当前有效性检查与前瞻性的未来必然性检查相结合，他们可以提供比标准监控更早、更有用的结论。该系统不会预测随机的故障或传感器故障，因为它并不针对未建模的异常；它预测的是机器人自身设计的逻辑后果。在复杂且充满不确定性的自主机器人世界中，这种能够洞察正确路径必然结果的能力，提供了一种全新的安全保障，将响应式警报转变为前瞻性的引导。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。