用形式化验证确保时间规划问题无解的可信认证
Formally Verified Certification of Unsolvability of Temporal Planning Problems
- 将时间规划转为时序自动机网络，用模型检测求解
- 通过形式化证明确保编码与检测结果正确
- 适合需要高可信度的航空航天、医疗系统规划
我们提出一种时间规划问题无解认证的方法。该方法将规划问题编码为时序自动机网络，利用高效模型检测器进行分析，并通过已有的形式化验证证书检查器对结果进行认证。整个流程强调认证的可信性：我们使用Isabelle/HOL定理证明器对编码过程进行了形式化验证，同时采用另一已在Isabelle/HOL中形式化验证过的证书检查器来确认模型检测结果的正确性。
原文摘要 · Abstract (English)
We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。