Infinite-State Systems & VASS
I study the reachability problem and related decision problems for Vector Addition Systems with States (VASS), with a focus on low-dimensional instances and their complexity. My work establishes tight complexity bounds within the Grzegorczyk hierarchy and introduces geometric notions of dimension to extend these results.
Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This article introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates an increase in the solved rate, showing a 36.7% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.
Reachability of vector addition systems with states (VASS) is Ackermann complete. For d-dimensional VASS reachability it is known that the problem is NP-complete when d=1, PSPACE-complete when d=2, and in F_d when d>2. A geometrically d-dimensional VASS is a D-dimensional VASS for some D≥d such that the space spanned by the displacements of the circular paths admitted in the D-dimensional VASS is d-dimensional. It is proved that the F_d upper bounds remain valid for the reachability problem in the geometrically d-dimensional VASSes with d>2.
Due to the general undecidable results, verification of concurrent programs is a big challenge. Most existing verifiers adopt Petri net and its extensions based on abstraction and approximation as their verification models, which yet suffer from intractable complexity and are thus challenging to be efficient and complete. We choose Basic Parallel Process (BPP), a subclass of Petri nets, as the backbone verification model for verifying concurrent programs due to its lower complexity. We propose BPPChecker, the first model checker for verifying a subclass of CTL on BPP. A constraint-based algorithm is given in which formulas are handled by SMT solver Z3. Our approach involves introducing a k-step semantics for the EG operator. By doing so, we reduce the problem of deciding the satisfiability of EG-formulas and EF1-formulas to the problem of deciding the satisfiability of linear integer arithmetic formulas. Besides, we encode the Actor Communicating System (ACS), a program model for asynchronously communicating programs, to BPP. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.
An F_d upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where F_d 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 F_{d+4} upper bound due to Leroux and Schmitz (LICS 2019).
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.
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 F_7 established by Leroux and Schmidt in 2019.
In this paper, we propose a uniform interaction theory that covers both classical and randomized models. Under this framework, two basic relations, the equality relation within a model and the expressiveness relation between different models, are restudied. We also give an interesting comparison between the world of classical models and the world of randomized models.
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 carry out a quantitative study of the complexity of nondeterminism. The main contributions include: a summary of existing work on VAS reachability, coverability, and boundedness; a new understanding of the KLMST algorithm via decomposition-dimension reduction; and results on the growth rate of C-graphs characterizing worst-case branching time complexity.
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.
Computer Vision
Image restoration still poses significant challenges due to the complexity and diversity of real-world degradations. However, such degradations often manifest as spatially non-uniform, locally concentrated, and irregular patterns, which calls for a restoration model that can adapt its feature sampling to the underlying degradation geometry while remaining computationally efficient. In this paper, we design a novel image restoration framework built on a deformable restoration Transformer, termed DeRestormer. DeRestormer adapts to irregular but localized degradations via deformable attention, where a small set of sampling positions is learned to pre-filter and highlight key elements, so the model can better focus on informative regions and handle complex degradation patterns efficiently. In addition, we incorporate deformable convolutions at the bottleneck stage to dynamically adjust sampling locations across different scales, thus facilitating flexible multi-scale aggregation and effective integration of fine-grained details and global context. Extensive experiments on 13 datasets across 4 tasks demonstrate the effectiveness of DeRestormer, since it achieves state-of-the-art performance across a wide range of image restoration scenarios.
Haze removal remains a challenging problem, especially in complex scenarios involving occlusion and varying fog intensities. Most existing methods perform well on specific datasets or scenes. However, they often fail to generalize because they focus only on haze regions, ignoring their interaction with surrounding objects. To address this issue, we propose a contrastive learning framework that works dynamically at the patch level. It captures the relationships between hazy and haze-free regions to handle varying fog intensities. The framework uses brightness differences between hazy and haze-free images to evaluate fog intensity. Based on this evaluation, the framework dynamically selects appropriate positive and negative samples, enhancing the model's flexibility and efficacy. To further improve the robustness, we adopt a gray-scale image processing mechanism to convert RGB images to grayscale images. This reduces the light source interference and enables the network to focus on structural and contrast details. In addition, our novel feature extraction module combines long-range and short-range attention mechanisms to preserve the structural integrity of neighboring patches while modeling long-range dependencies. Experimental results show that our method can achieve better performance than that of the state-of-the-art approaches.
Accurate segmentation of lung nodules from computed tomography (CT) scans is crucial for lung cancer prevention and early diagnosis. However, this task is challenging due to the varying sizes, irregular shapes, inconsistent densities of lung nodules, and the visual similarity between nodules and surrounding tissues. To overcome these challenges, we propose a novel Multi-Window Uncertainty-Guided Segmentation Network (MUS-Net). This network learns diverse features of lung nodules from CT images under different window settings, enhancing segmentation accuracy. Specifically, we introduce an uncertainty indication module that provides Multi-Window Mask (MWM), effectively combining segmentation predictions from lung and mediastinal window settings. This innovative approach allows the network to identify regions of varying segmentation uncertainty, thereby enhancing the model's sensitivity to complex nodule boundaries and density variations. Furthermore, we incorporate a feature filter module to specifically enhance the learning of features from images under different window settings. Our extensive experiments on the LIDC-IDRI dataset demonstrate that our MUS-Net outperforms existing methods, significantly improving segmentation accuracy and robustness against nodule variability.
Traditional single-model approaches can achieve good performance in single-weather-affected images, but usually fail to restore real-world degraded images. This can be attributed to their reliance on weather-specific priors, while real-world weather degradation is typically caused by a combination of weather conditions. To address this limitation, we propose a Multi-Component Decomposition Network (MCD-Net), introducing a novel three-component prior designed to represent background content, primary degradation masks, and residual degradations separately. The proposed network employs multiple attention-guided branches to disentangle different degradation components from the multi-scale features extracted by the Transformer-based trunk network. Then the trunk output is decomposed into grouped features and dynamically assigned to branches with a fully connected layer to jointly estimate the clean background and the degraded input. Comprehensive experiments on four types of single-weather datasets and one multiple-weather degraded dataset validate that our MCD-Net significantly outperforms state-of-the-art methods, especially under challenging mixed-weather conditions.
Trustworthy AI
English writing assessment plays a pivotal role in language learning, yet manual scoring is labour-intensive and subjective. Automated essay scoring (AES) systems offer objective and scalable solutions. However, existing AES models often overlook genre-specific traits, limiting their accuracy. This paper introduces a genre-aware AES approach that integrates BERT for feature extraction and LSTM for trait scoring, alongside a large language model (ChatGLM) for feedback generation. Experiments on the ASAP dataset demonstrate our model's superior performance, achieving a Quadratic Weighted Kappa (QWK) score of 0.794. This approach not only enhances scoring accuracy but also provides constructive, genre-specific feedback, supporting students' writing development.
Long-tailed data is ubiquitous in real-world applications, posing significant challenges due to imbalanced class distribution and high levels of label noise. Previous methods to address long-tailed data with label noise often incur high computational and manual costs. To address these challenges, we propose a novel two-stage active label cleaning strategy, which extends active learning beyond traditional label acquisition to efficiently identify and correct mislabeled samples while minimizing annotation cost. Specifically, in the first stage, we propose a Balanced Class-Centered Contrastive Learning (BCCL) to enhance feature representation quality and identify potential label noise within long-tailed datasets. BCCL achieves this through a novel loss function that integrates contrastive learning with weighted average of class centers. The second stage employs an uncertainty-based active learning sorted sampling to retrain on potential label noise samples, focusing on high-uncertainty instances to determine the final noise samples needing to be relabeled. Our two-stage active label cleaning strategy minimizes the amount of data requiring re-annotation, ultimately improving classification performance through iterative re-labeling, while optimizing the use of annotation resources and reducing the annotation workload. Experimental results demonstrate the robustness of our proposed method across varying noise ratios and levels of imbalance, effectively enhancing discriminative capability on noisy data in multiple datasets and achieving superior classification performance on long-tailed data, particularly in high-noise scenarios.