时序规划问题不可解性的形式化验证认证
计算机科学中的逻辑
2025-10-21 v2 人工智能
摘要
我们提出一种时序规划不可解性认证的方法。该方法基于将规划问题编码为timed automata 网络，然后使用高效模型检查器对网络进行检查，随后使用证书检查器对模型检查器的输出进行认证。我们的 method 注重认证的可信度：我们使用 Isabelle/HOL 形式化地验证了将问题编码为timed automata 的实现，并使用另一个在 Isabelle/HOL 中形式化验证的现有证书检查器对模型检查结果进行认证。
引用
@article{arxiv.2510.10189,
title = {Formally Verified Certification of Unsolvability of Temporal Planning Problems},
author = {David Wang and Mohammad Abdulaziz},
journal= {arXiv preprint arXiv:2510.10189},
year = {2025}
}