Improved Algorithm for Reachability in d-VASS

(with Yuxi Fu and Yangluo Zheng)
In Proceedings of the 51st EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2024), Volume 297, pp. 136:1-136:18,2024

Abstract | Paper

An Fd upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where Fd is the d-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the 2-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the Fd+4 upper bound due to Leroux and Schmitz (LICS 2019).

Branching Bisimulation Semantics for Quantum Processes

(with Huan Long and Hao Wu)
Information Processing Letters, Volume 186, August 2024, 106492, 2024

Abstract | Paper

The qCCS model proposed by Feng et al. provides a powerful framework to describe and reason about quantum communication systems that could be entangled with the environment. However, they only studied weak bisimulation semantics. In this paper we propose a new branching bisimilarity for qCCS and show that it is a congruence. The new bisimilarity is based on the concept of ϵ-tree and preserves the branching structure of concurrent processes where both quantum and classical components are allowed. Furthermore, we present a polynomial time equivalence checking algorithm for the ground version of our branching bisimilarity.

Reachability in 3-VASS is in Tower

(with Yuxi Fu)
arXiv:2306.05710

Abstract | Paper

The reachability problem for vector addition systems with states (VASS) is Ackermann-complete. For every k ≥ 3, a completeness result for the k-dimensional VASS reachability problem is not yet available. It is shown in this paper that the 3-dimensional VASS reachability problem is in Tower, improving upon the current best upper bound F7 established by Leroux and Schmidt in 2019.

The Study of Vector Addition System

Phd. Thesis

Abstract | Paper

This thesis first focuses on the vector addition system. Based on the discussion of the existing work, we propose some new understanding of the reachability problem, which will help future research. Next, we focus on the nondeterministic computation, we will carry out quantitative study of the complexity of nondeterminism. AS far as we know, this is the first of it kind. The main contributions of the thesis are the follows:

  • First we summarize the existing work of VAS in the recent 60 years including reachability problem, coverability problem and boundedness problem. Especially for the lower bound of reachability problem, we compare with different techniques, which will help some related ver- ification problems in other models.
  • Next for the famous KLMST algorithm, we offer a new understanding of the algorithm, i.e. by the form of decomposition-dimension reduction-decomposition-· · · . In this way we try to build a relationship between the reachability problem for (𝑛 + 1)-dimensional VAS and the reachability problem for 𝑛-dimensional VAS, which we believe will contributes to efforts in the reachability problem for fixed dimension.
  • Finally for the abstract presentation of finite state computational objects C-graphs, we introduce the concept of height, which characterizes the maximal number of steps a computational object may engage. Then we give a recursive equality of the number of the C-graphs of height , and prove that its growth rate is non-elementary. This result classifies the worst case branching time complexity.

Counting nondeterministic computations

(with Yuxi Fu)
Theoretical Computer Science, Volume 897, 2 January 2022, Pages 49-63, 2022

Abstract | Paper

The structure of nondeterministic computations is extremely complicated. C-graphs are abstract representations of the branching structure of nondeterministic computations. The paper investigates the structure of finite state nondeterministic computations by showing that the complexity of the structure increases non-elementarily while the number of computation steps increases. This is achieved by establishing a recursive equation relating the number of C-graphs of a certain height to the number of C-graphs of smaller height.