TLDR: Researchers David Wang and Mohammad Abdulaziz introduce a formally verified method to certify the unsolvability of temporal planning problems. They encode planning problems into timed automata, and critically, the encoding process itself is mathematically proven correct using Isabelle/HOL, ensuring high trustworthiness in claims that a problem has no solution.
Artificial intelligence (AI) planning systems have made significant advancements, enabling them to tackle complex real-world problems. However, as these systems become more sophisticated, ensuring the trustworthiness of their outputs becomes increasingly vital. This is particularly true when a planner declares that a problem is “unsolvable” – meaning no sequence of actions can achieve the desired goal.
A new research paper, titled “Formally Verified Certification of Unsolvability of Temporal Planning Problems”, addresses this challenge for temporal planning. Temporal planning involves scenarios where actions have durations and can occur simultaneously, making the planning process inherently more complex than traditional sequential planning.
The Challenge of Trustworthy Unsolvability Claims
When an AI planner finds a solution, the plan itself acts as a certificate; one can simply execute or simulate it to confirm its validity. However, proving that a problem has *no* solution is much harder. Such “unsolvability certificates” can be incredibly long and complex, making them difficult to check manually or even with automated tools. The complexity of state-of-the-art planning algorithms further compounds this issue, raising questions about the reliability of their “unsolvable” declarations.
A Novel Approach: Encoding into Timed Automata
The researchers, David Wang and Mohammad Abdulaziz from King’s College London, propose an innovative approach. They convert the temporal planning problem into a “network of timed automata.” Timed automata are mathematical models designed to describe systems whose behavior is dependent on time. Once the planning problem is represented in this form, an efficient “model checker” can be used to determine if a solution exists within the timed automata network.
The Power of Formal Verification
The core of this work lies in its commitment to trustworthiness. While using a model checker on timed automata is a known technique, the crucial step here is the *formal verification* of the encoding process itself. This means that the translation from a temporal planning problem to a network of timed automata is mathematically proven to be correct. This rigorous proof is carried out using a powerful theorem prover called Isabelle/HOL.
By formally verifying the encoding, the researchers ensure that if the model checker finds the timed automata network to be unsolvable, this directly and reliably implies that the original temporal planning problem is also unsolvable. They also leverage an existing certificate checker for timed automata model checking, which has also been formally verified in Isabelle/HOL, further bolstering the trustworthiness of the entire system.
Simplified Semantics and Broader Applicability
To facilitate this complex verification, the authors devised a simpler semantics for temporal planning, which was then proven equivalent to more general semantics. This engineering decision made the mathematical reasoning about the encoding more manageable. Their approach also relaxes some conditions found in previous work, allowing for a more general notion of plan validity and permitting concurrent “snap action” execution, which means multiple instantaneous events can happen at the same time.
Also Read:
- Navigating Crowded Spaces: A New Hybrid Approach to Multi-Agent Pathfinding
- Extended Triangular Method: Advancing Automated Deduction with Dynamic Multi-Clause Reasoning
Looking Ahead
This work represents a significant step towards creating highly trustworthy AI planning systems. By providing strong guarantees for unsolvability claims in temporal planning, it opens doors for more reliable AI applications in critical domains. Future work includes formally proving the equivalence of their abstract temporal planning formulation with a subset of PDDL (Planning Domain Definition Language) and developing an executable certificate checker compatible with their system.
