Source author record

Xiaoxiao Yang

Xiaoxiao Yang appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Programming Languages Computer Vision Robotics

Catalog footprint

What is connected

6works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2024arXiv

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation

The verification of linearizability -- a key correctness criterion for concurrent objects -- is based on trace refinement whose checking is PSPACE-complete. This paper suggests to use \emph{branching} bisimulation instead. Our approach is based on comparing an abstract specification in which object methods are executed atomically to a real object program. Exploiting divergence sensitivity, this also applies to progress properties such as lock-freedom. These results enable the use of \emph{polynomial-time} divergence-sensitive branching bisimulation checking techniques for verifying linearizability and progress. We conducted the experiment on concurrent lock-free stacks to validate the efficiency and effectiveness of our methods.

preprint2022arXiv

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.

preprint2020arXiv

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.

preprint2016arXiv

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.

preprint2011arXiv

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.

preprint2010arXiv

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.