{"ID":2857102,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.10189","arxiv_id":"2510.10189","title":"Formally Verified Certification of Unsolvability of Temporal Planning Problems","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.","short_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 priorit...","url_abs":"https://arxiv.org/abs/2510.10189","url_pdf":"https://arxiv.org/pdf/2510.10189v2","authors":"[\"David Wang\",\"Mohammad Abdulaziz\"]","published":"2025-10-11T11:57:25Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\"]","methods":"[]","has_code":false}