Formally Verified Certification of Unsolvability of Temporal Planning Problems
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917026195308544 |
|---|---|
| author | Wang, David Abdulaziz, Mohammad |
| author_facet | Wang, David Abdulaziz, Mohammad |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_10189 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formally Verified Certification of Unsolvability of Temporal Planning Problems Wang, David Abdulaziz, Mohammad Logic in Computer Science Artificial Intelligence 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. |
| title | Formally Verified Certification of Unsolvability of Temporal Planning Problems |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2510.10189 |