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.

翻译：本文提出了一种时序规划无解性认证方法。该方法通过将规划问题编码为时间自动机网络，随后采用高效模型检测器对网络进行分析，并利用证书检查器对模型检测结果进行认证。本方法以认证可信度为核心设计目标：我们使用定理证明器Isabelle/HOL对时间自动机编码实现进行了形式化验证，并采用现有证书检查器（同样在Isabelle/HOL中完成形式化验证）对模型检测结果进行认证。