Qingliang Chen

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.

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.

AAAI Conference 2019 Conference Paper

Bi-Kronecker Functional Decision Diagrams: A Novel Canonical Representation of Boolean Functions

• Xuanxiang Huang
• Kehang Fang
• Liangda Fang
• Qingliang Chen
• Zhao-Rong Lai
• Linfeng Wei

In this paper, we present a novel data structure for compact representation and effective manipulations of Boolean functions, called Bi-Kronecker Functional Decision Diagrams (BKFDDs). BKFDDs integrate the classical expansions (the Shannon and Davio expansions) and their bi-versions. Thus, BKFDDs are the generalizations of existing decision diagrams: BDDs, FDDs, KFDDs and BBDDs. Interestingly, under certain conditions, it is sufficient to consider the above expansions (the classical expansions and their bi-versions). By imposing reduction and ordering rules, BKFDDs are compact and canonical forms of Boolean functions. The experimental results demonstrate that BKFDDs outperform other existing decision diagrams in terms of sizes.

KER Journal 2019 Journal Article

Principles and practice of multi-agent systems

• Qingliang Chen
• Paolo Torroni
• Serena Villata

IJCAI Conference 2016 Conference Paper

Reconfigurability in Reactive Multiagent Systems

• Xiaowei Huang
• Qingliang Chen
• Jie Meng
• Kaile Su

Reactive agents are suitable for representing physical resources in manufacturing control systems. An important challenge of agent-based manufacturing control systems is to develop formal and structured approaches to support their specification and verification. This paper proposes a logic-based approach, by generalising that of model checking multiagent systems, for the reconfigurability of reactive multiagent systems. Two reconfigurability scenarios are studied, for the resulting system being a monolithic system or an individual module, and their computational complexity results are given.

AAAI Conference 2016 Conference Paper

Strengthening Agents Strategic Ability with Communication

• Xiaowei Huang
• Qingliang Chen
• Kaile Su

The current frameworks of reasoning about agents’ collective strategy are either too conservative or too liberal in terms of the sharing of local information between agents. In this paper, we argue that in many cases, a suitable amount of information is required to be communicated between agents to both enforce goals and keep privacy. Several communication operators are proposed to work with an epistemic strategy logic ATLK. The complexity of model checking resulting logics is studied, and surprisingly, we found that the additional expressiveness from the communication operators comes for free.

IJCAI Conference 2015 Conference Paper

The Complexity of Model Checking Succinct Multiagent Systems

• Xiaowei Huang
• Qingliang Chen
• Kaile Su

This paper studies the complexity of model checking multiagent systems, in particular systems succinctly described by two practical representations: concurrent representation and symbolic representation. The logics we concern include branching time temporal logics and several variants of alternating time temporal logics.

AAAI Conference 2010 Conference Paper

EWLS: A New Local Search for Minimum Vertex Cover

• Shaowei Cai
• Kaile Su
• Qingliang Chen

A number of algorithms have been proposed for the Minimum Vertex Cover problem. However, they are far from satisfactory, especially on hard instances. In this paper, we introduce Edge Weighting Local Search (EWLS), a new local search algorithm for the Minimum Vertex Cover problem. EWLS is based on the idea of extending a partial vertex cover into a vertex cover. A key point of EWLS is to find a vertex set that provides a tight upper bound on the size of the minimum vertex cover. To this purpose, EWLS employs an iterated local search procedure, using an edge weighting scheme which updates edge weights when stuck in local optima. Moreover, some sophisticated search strategies have been taken to improve the quality of local optima. Experimental results on the broadly used DIMACS benchmark show that EWLS is competitive with the current best heuristic algorithms, and outperforms them on hard instances. Furthermore, on a suite of difficult benchmarks, EWLS delivers the best results and sets a new record on the largest instance.

AAMAS Conference 2005 Conference Paper

A Computationally Grounded Logic of Knowledge, Belief and Certainty

• Kaile Su
• Abdul Sattar
• Guido Governatori
• Qingliang Chen