Yuxin Deng

AAAI Conference 2026 Conference Paper

SGPFeat: Semantic and Geometric Priors for Multi-modal Image Matching

• Yuxin Deng
• Botian Wang
• Kaining Zhang
• Hao Zhang
• Jiayi Ma

Multi-modal image matching is a fundamental task in multi-view and multi-modal image processing. Its key challenge lies in extracting features that remain consistent despite drastic appearance variations across modalities. However, the learning of the feature is hindered by the scarcity and the inaccurate alignment of existing multi-modal datasets. To address this, we propose a knowledge distillation framework termed SGPFeat that transfers rich prior knowledge from large-scale unimodal tasks to enhance multi-modal representation learning. Specifically, semantic priors from a vision foundation model guide the feature extractor to identify shared semantic structures across modalities, enabling better generalization under large appearance gaps. In parallel, geometric priors derived from accurately aligned visible-light datasets improve detection precision on noisy aligned multi-modal pairs. Furthermore, we introduce a Heterogeneous Feature Aggregation (HFA) module to facilitate effective distillation and feature representation. Extensive experiments demonstrate that semantic and geometric priors bring significant improvement for our SGPFeat across diverse multi-modal image matching benchmarks.

AAAI Conference 2025 Conference Paper

BEVSync: Asynchronous Data Alignment for Camera-based Vehicle-Infrastructure Cooperative Perception Under Uncertain Delays

• Wentao Wang
• Jiaqian Wang
• Yuxin Deng
• Guang Tan

Vehicle-to-infrastructure (V2I) cooperative perception systems can enhance the sensing abilities of autonomous vehicles. Existing V2I solutions often consider LiDARs devices instead of cameras, the most prevalent sensors with low cost and wide installation. In addition, a major challenge that has been underexplored is the time asynchrony between image frames from different sources. This asynchrony arises because of clock differences, varying times involved in data processing and transmission, causing uncertain delays that complicate data alignment and potentially reduce perception accuracy. We propose BEVSync, a camera-based V2I cooperative perception system that adaptively aligns frames from the ego-vehicle and infrastructure by compensating for motion deviations. Specifically, we develop an extractor-compensator model to extract and predict perceptual features using historical frames, thereby smoothing out the data misalignment. Experiments on the real-world dataset DAIR-V2X show that our approach surpasses existing methods in terms of performance and robustness.

AAAI Conference 2024 Conference Paper

ResMatch: Residual Attention Learning for Feature Matching

• Yuxin Deng
• Kaining Zhang
• Shihua Zhang
• Yansheng Li
• Jiayi Ma

Attention-based graph neural networks have made great progress in feature matching. However, the literature lacks a comprehensive understanding of how the attention mechanism operates for feature matching. In this paper, we rethink cross- and self-attention from the viewpoint of traditional feature matching and filtering. To facilitate the learning of matching and filtering, we incorporate the similarity of descriptors into cross-attention and relative positions into self-attention. In this way, the attention can concentrate on learning residual matching and filtering functions with reference to the basic functions of measuring visual and spatial correlation. Moreover, we leverage descriptor similarity and relative positions to extract inter- and intra-neighbors. Then sparse attention for each point can be performed only within its neighborhoods to acquire higher computation efficiency. Extensive experiments, including feature matching, pose estimation and visual localization, confirm the superiority of the proposed method. Our codes are available at https://github.com/ACuOoOoO/ResMatch.

AAAI Conference 2024 Conference Paper

SDGMNet: Statistic-Based Dynamic Gradient Modulation for Local Descriptor Learning

• Yuxin Deng
• Jiayi Ma

Rescaling the backpropagated gradient of contrastive loss has made significant progress in descriptor learning. However, current gradient modulation strategies have no regard for the varying distribution of global gradients, so they would suffer from changes in training phases or datasets. In this paper, we propose a dynamic gradient modulation, named SDGMNet, for contrastive local descriptor learning. The core of our method is formulating modulation functions with dynamically estimated statistical characteristics. Firstly, we introduce angle for distance measure after deep analysis on backpropagation of pair-wise loss. On this basis, auto-focus modulation is employed to moderate the impact of statistically uncommon individual pairs in stochastic gradient descent optimization; probabilistic margin cuts off the gradients of proportional triplets that have achieved enough optimization; power adjustment balances the total weights of negative pairs and positive pairs. Extensive experiments demonstrate that our novel descriptor surpasses previous state-of-the-art methods in several tasks including patch verification, retrieval, pose estimation, and 3D reconstruction.

TCS Journal 2023 Journal Article

Preface for the special issue of Theoretical Computer Science in honor of the 60th birthday of Yuxi Fu

• Yijia Chen
• Pierre-Louis Curien
• Yuxin Deng
• Min Zhang

TCS Journal 2022 Journal Article

An algebraic method to fidelity-based model checking over quantum Markov chains

• Ming Xu
• Jianling Fu
• Jingyi Mei
• Yuxin Deng

Fidelity is one of the most widely used quantities in quantum information that measures the distance of two quantum states through a noisy channel, a kind of quantum operations. In this paper, we consider the model of quantum Markov chain (QMC), in which transitions are weighted by super-operators to characterize quantum operations and the initial quantum state is left parametric. A quantum analogy of probabilistic computation tree logic, called QCTL, is introduced to take into account fidelity, instead of probability measure, over QMC. The key to the model checking problem lies in computing the fidelity of the super-operator valued measure specified by a path formula in QCTL. It is minimized over all initial quantum states, which is intended for analyzing the system performance in the worst case. We achieve it by a reduction to quantifier elimination in the existential theory of the reals. The method is absolutely exact, so that model checking QCTL formulas against QMCs is proved to be decidable in exponential time.

TCS Journal 2022 Journal Article

Formal semantics of a classical-quantum language

• Yuxin Deng
• Yuan Feng

We investigate the formal semantics of a simple imperative language that has both classical and quantum constructs. More specifically, we provide an operational semantics, a denotational semantics and two Hoare-style proof systems: an abstract one and a concrete one. The two proof systems are satisfaction-based, as inspired by the program logics of Barthe et al. for probabilistic programs. The abstract proof system turns out to be sound and relatively complete, while the concrete one is sound only.

TCS Journal 2022 Journal Article

Model checking QCTL plus on quantum Markov chains

• Ming Xu
• Jianling Fu
• Jingyi Mei
• Yuxin Deng

Verifying temporal properties of quantum systems, including quantum Markov chains (QMCs), has attracted an increasing interest in the last decade. Typically, the properties are specified by quantum computation tree logic (QCTL), in which reachability analysis plays a central role. However, safety as the dual problem is known little. Motivated by this, we propose a more expressive logic — QCTL+ (QCTL plus), which extends QCTL by allowing the conjunction in path formulas and the negation in the top level of path formulas. The former can be adopted to express conditional events, and the latter can express safety. To deal with conjunction, we present a product construction of classical states in the QMC and the tri-valued truths of atomic path formulas; to deal with negation, we develop an algebraic approach to compute the safety of the bottom strongly connected component subspaces with respect to a super-operator under some necessary and sufficient convergence conditions. Thereby we conditionally decide QCTL+ formulas over QMCs; without the convergence conditions the safety problem still remains open. The complexity of our method is provided in terms of the size of both the input QMC and the QCTL+ formula.

I&C Journal 2020 Journal Article

Time-bounded termination analysis for probabilistic programs with delays

• Ming Xu
• Yuxin Deng

This paper investigates the model of probabilistic program with delays (PPD) that consists of a few program blocks. Performing each block has an additional time-consumption—waiting to be executed—besides the running time. We interpret the operational semantics of PPD by Markov automata with a cost structure on transitions. Our goal is to measure those individual execution paths of a PPD that terminates within a given time bound, and to compute the minimum termination probability, i. e. the termination probability under a demonic scheduler that resolves the nondeterminism inherited from probabilistic programs. When running time plus waiting time is bounded, the demonic scheduler can be determined by comparison between a class of well-formed real numbers. The method is extended to parametric PPDs. When only the running time is bounded, the demonic scheduler can be determined by real root isolation over a class of well-formed real functions under Schanuel's conjecture. Finally we give the complexity upper bounds of the proposed methods.

I&C Journal 2017 Journal Article

Probabilistic bisimilarity as testing equivalence

• Yuxin Deng
• Yuan Feng

Larsen and Skou initiated the study of probabilistic bisimilarity and its characterisation in terms of tests. Later on, van Breugel et al. showed that, for labelled Markov processes with continuous state spaces, probabilistic bisimilarity nicely coincides with a simple notion of testing equivalence. Their proof employs advanced machinery from topology. In the discrete case of finite-state reactive probabilistic processes, we prove that coincidence result with an elementary and more accessible proof.

TCS Journal 2015 Journal Article

Program equivalence in linear contexts

• Yuxin Deng
• Yu Zhang

Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual equivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.

TCS Journal 2014 Journal Article

Real-reward testing for probabilistic processes

• Yuxin Deng
• Rob van Glabbeek
• Matthew Hennessy
• Carroll Morgan

We introduce a notion of real-valued reward testing for probabilistic processes by extending the traditional nonnegative-reward testing with negative rewards. In this richer testing framework, the may- and must-preorders turn out to be inverses. We show that for convergent processes with finitely many states and transitions, but not in the presence of divergence, the real-reward must-testing preorder coincides with the nonnegative-reward must-testing preorder. To prove this coincidence we characterise the usual resolution-based testing in terms of the weak transitions of processes, without having to involve policies, adversaries, schedulers, resolutions or similar structures that are external to the process under investigation. This requires establishing the continuity of our function for calculating testing outcomes.

I&C Journal 2013 Journal Article

On the semantics of Markov automata

• Yuxin Deng
• Matthew Hennessy

Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of reduction barbed congruence, the well-known touchstone equivalence for a large variety of process description languages.

TCS Journal 2007 Journal Article

Axiomatizations for probabilistic finite-state behaviors

• Yuxin Deng
• Catuscia Palamidessi

We study a process calculus which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s probabilistic automata. We consider various strong and weak behavioral equivalences, and we provide complete axiomatizations for finite-state processes, restricted to guarded recursion in case of the weak equivalences. We conjecture that in the general case of unguarded recursion the “natural” weak equivalences are undecidable. This is the first work, to our knowledge, that provides a complete axiomatization for weak equivalences in the presence of recursion and both nondeterministic and probabilistic choice.

I&C Journal 2006 Journal Article

Ensuring termination by typability

• Yuxin Deng
• Davide Sangiorgi

A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculus processes. The systems are obtained by successive refinements of the types of the simply typed π-calculus. For all (but one of) the type systems we also present upper bounds to the number of steps well-typed processes take to terminate. The termination proofs use techniques from term rewriting systems. We show the usefulness of the type systems on some non-trivial examples: the encodings of primitive recursive functions, the protocol for encoding separate choice in terms of parallel composition, a symbol table implemented as a dynamic chain of cells.

TCS Journal 2006 Journal Article

Towards an algebraic theory of typed mobile processes

• Yuxin Deng
• Davide Sangiorgi

The impact of types on the algebraic theory of the π -calculus is studied. The type system has capability types. They allow one to distinguish between the ability to read from a channel, to write to a channel, and both to read and to write. They also give rise to a natural and powerful subtyping relation. Two variants of typed bisimilarity are considered, both in their late and in their early version. For both of them, proof systems that are sound and complete on the closed finite terms are given. For one of the two variants, a complete axiomatisation for the open finite terms is also presented.