Automatic Verification of Linear Integer Planning Programs via Forgetting in LIAUPF

The goal of generalized planning (GP) is to find a generalized solution for a class of planning problems. One of effective means to solve GP is to transform a GP problem into an abstract planning problem, which can be easily solved. Recently, Lin et al. proposed a novel abstract model for GP, namely generalized linear integer numeric planning (GLINP), whose solution is an algorithmic-like structure called a planning program. They also developed an inductive approach to generating planning programs for GLINP. However, it has no theoretical guarantee that the generated planning program holds for infinitely many problem instances. To address this defect, we propose an automatic approach to verify whether the planning program works for infinitely many problem instances in this paper. We translate the planning program into a set of trace axioms finitely represented by linear integer arithmetic with uninterpreted predicate and function symbols (LIAUPF), and reduce the problem to the entailment problem of LIAUPF. Due to the undecidability of entailment problem in LIAUPF, we identify a class of planning programs whose trace axioms can be simplified in linear integer arithmetic (LIA), that is, a decidable fragment of LIAUPF, when reasoning about only the input and output of planning programs. As a result, the correctness verification of this class of programs becomes decidable.

Authors

• Liangda Fang Jinan University Pazhou Lab
• Shikang Chen Jinan University
• Xiaoman Wang Jinan University
• Xiaoyou Lin Jinan University
• Chenyi Zhang Institute of Information Science, Beijing Jiaotong University Visual Intelligence + X International Joint Laboratory of the Ministry of Education MT Lab, Meitu Inc.
• Qingliang Chen
• Quanlong Guan Jinan University
• Kaile Su

Keywords

• Generalized Planning
• Program Verification
• Linear Integer Arithmetic
• ∗Corresponding author.
• †Corresponding author.
• This work is licensed under a Creative Commons Attribution International 4. 0 License.
• Proc. of the 24th International Conference on Autonomous Agents and Multiagent Systems
• (AAMAS 2025)
• Y. Vorobeychik
• S. Das
• A. Nowé (eds.)
• May 19 – 23
• 2025
• Detroit
• Michigan
• USA. © 2025 International Foundation for Autonomous Agents and Multiagent Systems
• (www. ifaamas. org).