Weijun Chen

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.

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.

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.

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.