# Formally Verified Certification of Unsolvability of Temporal Planning Problems

arXiv: https://arxiv.org/abs/2510.10189 · HTML: https://mlsanity.com/paper/2510.10189/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 1 of its 47 references that are in the map.
- First posted on arXiv 11 Oct 2025.

## Builds on (most cited first, 1 of 1)

- [Formally Verified SAT-Based AI Planning](https://mlsanity.com/paper/2010.14648/) (2020)

## Abstract (arXiv)

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.