Formally Verified Certification of Unsolvability of Temporal Planning Problems
This provides a formally verified method for certifying unsolvability in temporal planning, which is incremental as it builds on existing model checking and verification techniques.
The paper tackles the problem of certifying unsolvability in temporal planning by encoding planning problems into timed automata and using model checking with formal verification, achieving a trustworthy certification process through Isabelle/HOL.
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.