arXiv subjects

Xiaoxiao Yang

Publications and source records attributed to Xiaoxiao Yang.

25 records · Page 2Linked to original sources

arXiv2022

A Miniature 3-DoF Flexible Parallel Robotic Wrist Using NiTi Wires for Gastrointestinal Endoscopic Surgery

Gastrointestinal endoscopic surgery (GES) has high requirements for instruments' size and distal dexterity, because of the narrow endoscopic channel and long, tortuous human gastrointestinal tract. This paper utilized Nickel-Titanium (NiTi) wires to develop a miniature 3-DoF (pitch-yaw-translation) flexible parallel robotic wrist (FPRW). Additionally, we assembled an electric knife on the wrist's connection interface and then teleoperated it to perform an endoscopic submucosal dissection (ESD) on porcine stomachs. The effective performance in each ESD workflow proves that the designed FPRW has sufficient workspace, high distal dexterity, and high positioning accuracy.

cs.RO↗

arXiv2021

BAANet: Learning Bi-directional Adaptive Attention Gates for Multispectral Pedestrian Detection

Thermal infrared (TIR) image has proven effectiveness in providing temperature cues to the RGB features for multispectral pedestrian detection. Most existing methods directly inject the TIR modality into the RGB-based framework or simply ensemble the results of two modalities. This, however, could lead to inferior detection performance, as the RGB and TIR features generally have modality-specific noise, which might worsen the features along with the propagation of the network. Therefore, this work proposes an effective and efficient cross-modality fusion module called Bi-directional Adaptive Attention Gate (BAA-Gate). Based on the attention mechanism, the BAA-Gate is devised to distill the informative features and recalibrate the representations asymptotically. Concretely, a bi-direction multi-stage fusion strategy is adopted to progressively optimize features of two modalities and retain their specificity during the propagation. Moreover, an adaptive interaction of BAA-Gate is introduced by the illumination-based weighting strategy to adaptively adjust the recalibrating and aggregating strength in the BAA-Gate and enhance the robustness towards illumination changes. Considerable experiments on the challenging KAIST dataset demonstrate the superior performance of our method with satisfactory speed.

cs.CV↗

arXiv2020

Learning Consistency Pursued Correlation Filters for Real-Time UAV Tracking

Correlation filter (CF)-based methods have demonstrated exceptional performance in visual object tracking for unmanned aerial vehicle (UAV) applications, but suffer from the undesirable boundary effect. To solve this issue, spatially regularized correlation filters (SRDCF) proposes the spatial regularization to penalize filter coefficients, thereby significantly improving the tracking performance. However, the temporal information hidden in the response maps is not considered in SRDCF, which limits the discriminative power and the robustness for accurate tracking. This work proposes a novel approach with dynamic consistency pursued correlation filters, i.e., the CPCF tracker. Specifically, through a correlation operation between adjacent response maps, a practical consistency map is generated to represent the consistency level across frames. By minimizing the difference between the practical and the scheduled ideal consistency map, the consistency level is constrained to maintain temporal smoothness, and rich temporal information contained in response maps is introduced. Besides, a dynamic constraint strategy is proposed to further improve the adaptability of the proposed tracker in complex situations. Comprehensive experiments are conducted on three challenging UAV benchmarks, i.e., UAV123@10FPS, UAVDT, and DTB70. Based on the experimental results, the proposed tracker favorably surpasses the other 25 state-of-the-art trackers with real-time running speed ($\sim$43FPS) on a single CPU.

cs.CV↗

arXiv2018

The Effect Race in Fine-Grained Concurrency

Most existed work require knowledge about the effect of program instructions (or statements) to analyze and verify algorithms. In this paper, by revealing some findings on executions of object programs, we define two basic concepts -- effect equivalence relation and effect race relation. Further, we show three effect theorems about the race and histories. The core result is that the effect race relation is the accurate relation to capture the internal steps, of which precedence orders are the reason to cause chaotic histories. In addition, the concept -- linearization points -- widely used in the object verification, is defined formally as the typical effect race relation. These results provide a clear basis for analyzing intricate fine-grained executions. We conduct a lot of experiments on real object algorithms to show the accuracy and efficiency of these definitions in practice. A simple quantitative analysis method for these algorithms is also proposed.

cs.PL↗

arXiv2016

Proving Linearizability via Branching Bisimulation

Linearizability and progress properties are key correctness notions for concurrent objects. However, model checking linearizability has suffered from the PSPACE-hardness of the trace inclusion problem. This paper proposes to exploit branching bisimulation, a fundamental semantic equivalence relation developed for process algebras which can be computed efficiently, in checking these properties. A quotient construction is provided which results in huge state space reductions. We confirm the advantages of the proposed approach on more than a dozen benchmark problems.

cs.PL↗

arXiv2011

A Probabilistic Variant of Projection Temporal Logic

In this paper, we propose Probabilistic discrete-time Projection Temporal Logic (PrPTL), which extends Projection Temporal Logic (PTL) with probability. To this end, some useful formulas are derived and some logic laws are given. Further, we define Time Normal Form (TNF) for PrPTL as the standard form and prove that any PrPTL formulas can be rewritten to TNF. According to the TNF, we construct the time normal form graph which can be used for the probabilistic model checking on PrPTL.

cs.LO↗

arXiv2010

Probabilistic Model Checking for Propositional Projection Temporal Logic

Propositional Projection Temporal Logic (PPTL) is a useful formalism for reasoning about period of time in hardware and software systems and can handle both sequential and parallel compositions. In this paper, based on discrete time Markov chains, we investigate the probabilistic model checking approach for PPTL towards verifying arbitrary linear-time properties. We first define a normal form graph, denoted by NFG_inf, to capture the infinite paths of PPTL formulas. Then we present an algorithm to generate the NFG_inf. Since discrete-time Markov chains are the deterministic probabilistic models, we further give an algorithm to determinize and minimize the nondeterministic NFG_inf following the Safra's construction.

cs.LO↗