publications

2026

1. Conference

   Improving Reachability in Vector Addition Systems Through Pumpability

   Weijun Chen, Yuxi Fu, and Yangluo Zheng

   In 37th International Conference on Concurrency Theory (CONCUR 2026), 2026

   Abs DOI arXiv PDF

   Vector addition systems (VAS) constitute an important model of computation and concurrency that is equally expressive as the Petri net model. Recently, a lot of research has been conducted on vector addition systems with states (VASS), which are VASes equipped with a finite state control. Results on VASS naturally carry over to VAS, but no straightforward improvement is available. In this paper, we investigate the reachability problem in VAS in fixed dimensions. Based on a pumpability analysis of VAS that refines Rackoff’s extraction for VASS, we obtain an $\textbf{F}_{d-2}$ upper bound for the d-dimensional VAS reachability problem, improving the $\textbf{F}_d$ upper bound inherited from the d-dimensional VASS reachability problem. Low-dimensional VASes are also considered. In particular, we establish a PSPACE upper bound for reachability in 4-dimensional VAS and an ELEMENTARY upper bound for 5-dimensional VAS, while the same upper bounds were known only for 2-VASS and 3-VASS, respectively. The result for 4-VAS particularly hinges on a simplified projection technique developed for geometrically 2-dimensional VASSes, whose reachability problem is shown to be equivalent to 2-VASS.

2. Journal

   A unifying approach to probabilistic testing equivalences

   Weijun Chen, Yuxi Fu, Huan Long, and Hao Wu

   Theor. Comput. Sci., Jun 2026

   Abs DOI arXiv

   Probabilistic concurrent systems are foundational models for modern mobile computing. In this paper, a unifying approach to probabilistic testing equivalences is proposed. With the help of a new distribution-based semantics for probabilistic models and a probabilistic testing framework with respect to process predicates, the internal characterization and the external characterization for testing equivalences are studied. The latter characterization can be viewed as the generalization of the classical fair/should equivalence and may equivalence. These equivalences are shown to be congruences. A thorough comparison between these equivalences and probabilistic bisimilarities is carried out. The techniques introduced in this paper can be easily extended to other probabilistic concurrent models. To showcase this flexibility, a case study is carried out on the pCSP model.

3. Journal

   Survey on Complexity Lower Bound Research for Reachability Problem in Vector Addition Systems

   Weijun Chen, Yuxi Fu, and Huan Long

   Ruan Jian Xue Bao/Journal of Software (In Chinese), Jan 2026

   Abs DOI

   Concurrency and scalability are fundamental properties of most complex systems. As a widely used formalism for modeling concurrency, Petri nets have been applied across various fields. Their mathematical abstraction, the vector addition system (VAS), has become a central object of study in theoretical computer science. The reachability problem of VAS, along with its algorithmic and complexity characterizations, has been regarded as one of the most fundamental and long-standing challenges in the field over the last 50 years. This study presents a comprehensive survey of the research on the complexity lower bounds of the VAS reachability problem. The definitions of VAS, their equivalent models, and the core verification problem, the reachability problem, are introduced. Known completeness results concerning the complexity of the reachability problem are reviewed. For the fixed-dimension case, proof frameworks based on multiplication triples and amplifiers are outlined, and the state-of-the-art achievements as well as core proof techniques are summarized. Finally, the current research bottlenecks, major open problems, and future challenges are discussed.

4. Preprint

   3-VASS Reachability is in EXPSPACE

   Weijun Chen, Bo Fu, Yuxi Fu, Huan Long, Chengfeng Xue, Qizhe Yang, and Yangluo Zheng

   2026

   Abs DOI arXiv

   A VASS can be viewed as a finite-state automaton manipulating a fixed number (called its dimension) of counters holding non-negative values. The reachability problem, asking whether there is a run from one configuration, defined by a state and values of the counters, to another configuration, has been a long-standing algorithmic challenge in theoretical computer science. When the dimension is part of the input, the problem has been shown to be ACKERMANN-complete in 2021. For fixed dimension greater than 2, and in particular for dimension 3, the exact complexity of the reachability problem remains unclear. For a long time the known algorithms for the 3-dimensional VASS reachability problem had been non-elementary, while the best known lower bound is merely PSPACE hardness inherited from dimension 2. A recent breakthrough in (Czerwiński, Jecker, Lasota, Orlikowski, ICALP 2025) gave the first elementary upper bound for the problem, namely 2-EXPSPACE. In this paper it is shown that the reachability problem in 3-VASS belongs to EXPSPACE. The proof is based on a hierarchical pumpability analysis, yielding a doubly-exponential length bound on the shortest runs between two configurations.

2025

1. Conference

   A Programming Language for Feasible Solutions

   Weijun Chen, Yuxi Fu, and Huan Long

   In Static Analysis - 32nd International Symposium, SAS 2025, Singapore, October 13-14, 2025, Proceedings, Oct 2025

   Abs DOI arXiv

   Runtime efficiency and termination are crucial properties in the studies of program verification. Instead of dealing with these issues in an ad hoc manner, it would be useful to develop a robust framework in which such properties are guaranteed by design. This paper introduces a new imperative programming language whose design is grounded in a static type system that ensures the following equivalence property: All definable programs are guaranteed to run in polynomial time; Conversely, all problems solvable in polynomial time can be solved by some programs of the language. The contribution of this work is twofold. On the theoretical side, the foundational equivalence property is established, and the proof of the equivalence theorem is non-trivial. On the practical side, a programming approach is proposed that can streamline program analysis and verification for feasible computations. An interpreter for the language has been implemented, demonstrating the feasibility of the approach in practice.