Formally Verified Certification of Unsolvability of Temporal Planning Problems
Logic in Computer Science
2025-10-21 v2 Artificial Intelligence
Abstract
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.
Keywords
Cite
@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}
}