Formally Verified Certification of Unsolvability of Temporal Planning Problems
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Unifying and Certifying Top-Quality Planning
The growing utilization of planning tools in practical scenarios has sparked an interest in generating multiple high-quality plans. Consequently, a range of computational problems under the general umbrella of top-qualit…
Formal Semantics and Formally Verified Validation for Temporal Planning
We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorit…
Exploring Inevitable Waypoints for Unsolvability Explanation in Hybrid Planning Problems
Explaining unsolvability of planning problems is of significant research interest in Explainable AI Planning. AI planning literature has reported several research efforts on generating explanations of solutions to planni…
PhilosophyWhy Couldn't You do that? Explaining Unsolvability of Classical Planning Problems in the Presence of Plan Advice
Explainable planning is widely accepted as a prerequisite for autonomous agents to successfully work with humans. While there has been a lot of research on generating explanations of solutions to planning problems, expla…
A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify th…