Author name cluster

Xiaoyou Lin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

AAMAS Conference 2025 Conference Paper

Automatic Verification of Linear Integer Planning Programs via Forgetting in LIAUPF

Liangda Fang
Shikang Chen
Xiaoman Wang
Xiaoyou Lin
Chenyi Zhang
Qingliang Chen
Quanlong Guan
Kaile Su

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.

PDF

ICAPS Conference 2022 Conference Paper

Generalized Linear Integer Numeric Planning

Xiaoyou Lin
Qingliang Chen
Liangda Fang
Quanlong Guan
Weiqi Luo 0002
Kaile Su

Classical planning aims to find a sequence of actions that guarantees goal achievement from an initial state. The representative framework of classical planning is based on propositional logic. Due to the weak expressiveness of propositional logic, many applications of interest cannot be formalized as a classical planning problem. Some extensions such as numeric planning and generalized planning (GP) are therefore proposed. Qualitative numeric planning (QNP) is a decidable class of numeric and generalized extensions and serves as a numeric abstraction of GP. However, QNP is still far from being perfect and needs further improvement. In this paper, we introduce another generalized version of numeric planning, namely generalized linear integer numeric planning(GLINP), which is a more suitable abstract framework of GP than QNP. In addition, we develop a general framework to synthesize solutions to GLINP problems. Finally, we evaluate our approach on a number of benchmarks, and experimental results justify the effectiveness and scalability of our proposed approach.

Details