VLDB 2026 Research / reviewers in the wild / expert
Xiaoxiao Yang
dblp:80/5062
· DBLP profile ↗
32ranked-venue papers
10as first author
20since 2021 · last 2026
—ORCID · conflict
Domains — the database's venue-derived domains; a paper can count in several
Artificial intelligence and machine learning · 9 · 3 first-author · 8 since 2021Applied, interdisciplinary, general and emerging computing · 8 · 2 first-author · 6 since 2021Graphics, computer vision, multimedia, augmented reality and games · 7 · 1 first-author · 6 since 2021Systems, architecture and hardware · 6 · 2 first-author · 4 since 2021Software engineering, systems software and programming languages · 5 · 2 first-authorTheory of computation · 5 · 2 first-author · 2 since 2021Databases, data management, data science and information retrieval · 2 · 2 first-author · 2 since 2021Security and privacy · 1 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | A Gradient-Based Causal Discovery Framework With Applications to Complex Industrial ProcessesabstractWith the rapid development of deep learning, a wide range of neural network-based causal discovery frameworks have emerged. Although these methods have achieved significant advancements, they still face several limitations when deployed in real-world industrial processes. Many existing models follow the component-wise modeling design, where an individual model must be built for each variable. This leads to significant computational overhead, especially in high-dimensional industrial systems. Moreover, imposing sparsity constraints on the first-layer weights of neural networks to discover causal relationships limits their ability to capture complex and nonlinear interactions among variables. To address these challenges, we propose a novel lightweight causal discovery framework, termed gradient-based causal discovery (GCD). Different from conventional component-wise models, GCD only employs a single multilayer perceptron for time-series prediction and leverages$\ell _{1}$regularization on the neural network’s input–output gradient to infer causal relationships. Numerical simulations on the Lorenz-96 and CausalTime show that GCD consistently achieves the state-of-the-art performance. Moreover, evaluations across four industrial processes, including Tennessee-Eastman, ultra-processed food, debutanizer, and gas turbine power generation, demonstrate that GCD significantly reduces computational overhead while maintaining high causal discovery accuracy, highlighting its applicability to complex industrial processes. Meiliang Liu, Huiwen Dong, Xiaoxiao Yang, Yunfang Xu, Mingbao Yang, Zhengye Si, Zhiwen Zhao |
IEEE Trans. Ind. Informatics | 3 |
| 2025 | SFNet: A Spatial-Frequency Domain Deep Learning Network for Efficient Alzheimer's Disease DiagnosisabstractAlzheimer's disease (AD) is a progressive neurodegenerative disorder that predominantly affects the elderly population and currently has no cure. Magnetic Resonance Imaging (MRI), as a non-invasive imaging technique, is essential for the early diagnosis of AD. MRI inherently contains both spatial and frequency information, as raw signals are acquired in the frequency domain and reconstructed into spatial images via the Fourier transform. However, most existing AD diagnostic models extract features from a single domain, limiting their capacity to fully capture the complex neuroimaging characteristics of the disease. While some studies have combined spatial and frequency information, they are mostly confined to 2D MRI, leaving the potential of dual-domain analysis in 3D MRI unexplored. To overcome this limitation, we propose Spatial-Frequency Network (SFNet), the first end-to-end deep learning framework that simultaneously leverages spatial and frequency domain information to enhance 3D MRI-based AD diagnosis. SFNet integrates an enhanced dense convolutional network to extract local spatial features and a global frequency module to capture global frequency-domain representations. Additionally, a novel multi-scale attention module is proposed to further refine spatial feature extraction. Experiments on the Alzheimer's Disease Neuroimaging Initiative (ADNI) dataset demonstrate that SFNet outperforms existing baselines and reduces computational overhead in classifying cognitively normal (CN) and AD, achieving an accuracy of 95.1%. Meiliang Liu, Yunfang Xu, Xiaoxiao Yang, Zhengye Si, Zhiwen Zhao |
BIBM | 4 |
| 2025 | ETSM: Automating Dissection Trajectory Suggestion and Confidence Map-Based Safety Margin Prediction for Robot-Assisted Endoscopic Submucosal DissectionabstractRobot-assisted Endoscopic Submucosal Dissection (ESD) improves the surgical procedure by providing a more comprehensive view through advanced robotic instruments and bimanual operation, thereby enhancing dissection efficiency and accuracy. Accurate prediction of dissection trajectories is crucial for better decision-making, reducing intraoperative errors, and improving surgical training. Nevertheless, predicting these trajectories is challenging due to variable tumor margins and dynamic visual conditions. To address this issue, we create the ESD Trajectory and Confidence Map-based Safety Margin (ETSM) dataset with 1849 short clips, focusing on submucosal dissection with a dual-arm robotic system. We also introduce a framework that combines optimal dissection trajectory prediction with a confidence map-based safety margin, providing a more secure and intelligent decision-making tool to minimize surgical risks for ESD procedures. Additionally, we propose the Regression-based Confidence Map Prediction Network (RCMNet), which utilizes a regression approach to predict confidence maps for dissection areas, thereby delineating various levels of safety margins. We evaluate our RCMNet using three distinct experimental setups: in-domain evaluation, robustness assessment, and out-of-domain evaluation. Experimental results show that our approach excels in the confidence map-based safety margin prediction task, achieving a mean absolute error (MAE) of only 3.18. To the best of our knowledge, this is the first study to apply a regression approach for visual guidance concerning delineating varying safety levels of dissection areas. Our approach bridges gaps in current research by improving prediction accuracy and enhancing the safety of the dissection process, showing great clinical significance in practice. The dataset and code are available at https://github.com/FrankMOWJ/RCMNet. Mengya Xu, Wenjin Mo, Guankun Wang, Huxin Gao, An Wang 0007, Long Bai 0008, Chaoyang Lyu, Xiaoxiao Yang, Zhen Li 0026, Hongliang Ren 0001 |
ICRA | 8 |
| 2025 | CoPESD: A Multi-Level Surgical Motion Dataset for Training Large Vision-Language Models to Co-Pilot Endoscopic Submucosal Dissection
Guankun Wang, Han Xiao 0010, Renrui Zhang, Huxin Gao, Long Bai 0008, Xiaoxiao Yang, Zhen Li 0026, Hongsheng Li 0001, Hongliang Ren 0001 |
ACM Multimedia | 6 |
| 2025 | On the Windy k-Traveling Salesman Problem
Xiaoxiao Yang, Junran Lichen, Runtao Xie |
TAMC | 2 |
| 2025 | Inducing Long-Term Plastic Changes and Visual Attention Enhancement Via One-Week Cerebellar Crus II Intermittent Theta Burst Stimulation (iTBS): An EEG StudyabstractIntermittent theta burst stimulation (iTBS) is a non-invasive technique frequently employed to induce neural plastic changes and enhance visual attention. Currently, most studies utilized a single iTBS session on healthy subjects to induce short-term neural plastic changes within tens of minutes post-stimulation and investigate its single-session effect on attention performance. Few studies have conducted multiple iTBS sessions on the cerebellum to explore long-term effects on the cerebral cortex and daily effects on visual attention performance. In this study, 18 healthy subjects were involved in a randomized, sham-controlled experiment over one week. All the subjects received daily session of bilateral cerebellar Crus II iTBS or sham stimulation and completed a visual search task. Resting-state electroencephalogram (EEG) was collected 48 hours pre- and post-experiment to assess plastic changes induced by iTBS. The results indicated that the iTBS group exhibited higher accuracy and lower time costs than the sham group after three sessions of iTBS. In addition, iTBS-induced plastic changes persisted up to 48 hours post-experiment, including left-shifted individual alpha frequency, increased intrinsic excitability (the likelihood that a neuron will generate an output in response to a given input), and enhanced PLV functional connectivity (phase synchronization between different brain region). Furthermore, we found that cerebellar iTBS induced a remote effect on the frontal region. Our study revealed the capacity of cerebellar Crus II iTBS to induce plastic changes and enhance attention performance, providing a potential avenue for using iTBS to promote rehabilitation. Meiliang Liu, Minjie Tian, Jingping Shi, Yunfang Xu, Zhengye Si, Xiaoxiao Yang, Li Yao 0002, Kuiying Yin, Zhiwen Zhao |
IEEE J. Biomed. Health Informatics | 8 |
| 2025 | AMFD: Distillation via Adaptive Multimodal Fusion for Multispectral Pedestrian DetectionabstractMultispectral pedestrian detection has been shown to be effective in improving performance in complex illumination scenarios. However, prevalent double-stream networks in multispectral detection employ two separate feature extraction branches for multi-modal data, leading to nearly double the inference time compared to single-stream networks utilizing only one feature extraction branch. This increased inference time has hindered the widespread employment of multispectral pedestrian detection in embedded devices for autonomous systems. To efficiently compress multispectral object detection networks, we propose a novel distillation method, the Adaptive Modal Fusion Distillation (AMFD) framework. Unlike traditional distillation methods, the AMFD framework fully leverages the original modal features from the teacher network, thereby significantly enhancing the performance of the student network. Specifically, a Modal Extraction Alignment (MEA) module is utilized to derive learning weights for student networks, integrating focal and global attention mechanisms. This methodology enables the student network to acquire optimal fusion strategies independent from that of teacher network without necessitating an additional feature fusion module. Furthermore, we present the SMOD dataset, a well-aligned challenging multispectral dataset for detection. Extensive experiments on the challenging KAIST, LLVIP, SUNRGB-D and SMOD datasets are conducted to validate the effectiveness of AMFD. The results demonstrate that our method outperforms existing state-of-the-art methods in both reducing log-average Miss Rate and improving mean Average Precision. The code is available athttps://github.com/bigD233/AMFD.git. Zizhao Chen, Yeqiang Qian, Xiaoxiao Yang, Ming Yang 0002 |
IEEE Trans. Multim. | 3 |
| 2024 | Spatial-Temporal Mamba Network for EEG-Based Motor Imagery Classification
Xiaoxiao Yang, Ziyu Jia |
ADMA (3) | 1 |
| 2024 | Towards Accurate 3D Face Alignment Under Extreme Scenarios Via Multi-Granularity Perturbation Relearningabstract3D face alignment from monocular images in challenging scenarios such as large poses and occlusions presents a huge challenge. To overcome this challenge, we propose a Multi-granularity Perturbation Relearning Network (MPRN), utilizing relearning attention to capture crucial features. Specifically, MPRN employs an attention mechanism to highlight effective features and further conducts relearning for attention to refine its accuracy. However, in extreme scenarios, the loss of key 3D facial information hampers the effective functioning of relearning attention. To this end, we construct multi-granularity perturbation graphs to infer the missing key 3D facial information and correspondingly guide the multiple times learning of attention module using perturbation graphs at various granularities. By doing this, our MPRN could effectively capture crucial 3D facial features in extreme scenarios, thereby achieving precise 3D face alignment. Experiments on the AFLW 2000-3D and AFLW datasets demonstrate the effectiveness of our MPRN. Xinyu Li 0014, Xiaoxiao Yang, Suping Wu, Xiangzheng Li, Xitie Zhang |
ICME | 3 |
| 2024 | OSSAR: Towards Open-Set Surgical Activity Recognition in Robot-assisted SurgeryabstractIn the realm of automated robotic surgery and computer-assisted interventions, understanding robotic surgical activities stands paramount. Existing algorithms dedicated to surgical activity recognition predominantly cater to pre-defined closed-set paradigms, ignoring the challenges of real-world open-set scenarios. Such algorithms often falter in the presence of test samples originating from classes unseen during training phases. To tackle this problem, we introduce an innovative Open-Set Surgical Activity Recognition (OSSAR) framework. Our solution leverages the hyperspherical reciprocal point strategy to enhance the distinction between known and unknown classes in the feature space. Additionally, we address the issue of over-confidence in the closed set by refining model calibration, avoiding misclassification of unknown classes as known ones. To support our assertions, we establish an open-set surgical activity benchmark utilizing the public JIGSAWS dataset. Besides, we also collect a novel dataset on endoscopic submucosal dissection for surgical activity tasks. Extensive comparisons and ablation experiments on these datasets demonstrate the significant outperformance of our method over existing state-of-the-art approaches. Our proposed solution can effectively address the challenges of real-world surgical scenarios. Our code is publicly accessible at github.com/longbai1006/OSSAR. Long Bai 0008, Guankun Wang, Jie Wang 0097, Xiaoxiao Yang, Huxin Gao, An Wang 0007, Mobarakol Islam, Hongliang Ren 0001 |
ICRA | 4 |
| 2024 | LighTDiff: Surgical Endoscopic Image Low-Light Enhancement with T-Diffusion
Tong Chen 0011, Qingcheng Lyu, Long Bai 0008, Erjian Guo, Huxin Gao, Xiaoxiao Yang, Hongliang Ren 0001, Luping Zhou |
MICCAI (6) | 6 |
| 2023 | An Efficient Hybrid Graph Network Model for Traveling Salesman Problem with Drone
Xiaoxiao Yang |
Neural Process. Lett. | 2 |
| 2023 | SAVAnet: Surgical Action-Driven Visual Attention Network for Autonomous Endoscope ControlabstractAn endoscope holder must understand the detailed surgical actions and the surgeons’ visual attention to keep important targets in the field of endoscopic view during operations. From an intensive analysis of the surgeons’ attention mechanism, we included that surgical actions, like cutting, suturing, etc., play an important role in determining the positions and weights of visual attention points during a dynamic surgical scene. To perform this process, this work proposes a Surgical Action-driven Visual Attention network (SAVAnet) and applies the network in autonomous endoscope control. Four scenarios are constructed in the da Vinci V-rep simulator: pick&place and needle exercise in a general laparoscopic training environment, needle driving with and without obstacle removal in an abdominal cavity, to create datasets for network training. The results show that the network has an outstanding performance in surgical action prediction with a high average accuracy of over 91%. Additionally, with surgical action guidance, the attention point prediction has higher accuracy and accords with surgeons’ visual attention. Finally, the acquired attention points are utilized to execute visual servoing in simulation. The results verify that the SAVAnet is feasible for autonomous endoscope control in real-time and lays a theoretical foundation for future sim-to-real execution. Note to Practitioners—This paper was motivated by the problem of endowing an endoscope with surgeons’ visual attention mechanism, which is affected by surgical actions, for autonomous endoscope control. An eye-tracking device has been utilized to detect surgeon’s visual attention in real-time and then control the endoscope to follow what the surgeon is looking at. However, this approach is susceptible to the surgical environment. Besides, many instrument detection and segmentation algorithms are developed for automatic surgical instrument tracking. However, surgeons’ visual attention does not always focus on the instruments during operations. In this work, we propose a novel SAVAnet to determine visual attention based on surgical actions. We prove from many qualitative and quantitative experiments that surgical actions play a significant role in determining visual attention. The designed SAVAnet can predict surgical actions correctly and then effectively guide the choice of visual attention. Finally, the simulation results show that the SAVAnet can endow endoscope with surgeons’ visual attention to perform self-control in real time. In future research, we will train the SAVAnet using real datasets and conduct more physical experiments on real surgical robots. Huxin Gao, Weichen Fan, Liang Qiu 0002, Xiaoxiao Yang, Zhen Li 0026, Xiuli Zuo, Max Q.-H. Meng, Hongliang Ren 0001 |
IEEE Trans Autom. Sci. Eng. | 4 |
| 2023 | AMagPoseNet: Real-Time Six-DoF Magnet Pose Estimation by Dual-Domain Few-Shot Learning From Prior ModelabstractTraditional magnetic tracking approaches based on mathematical models and optimization algorithms are computationally intensive, depend on initial guesses, and do not guarantee convergence to a global optimum. Although fully supervised data-driven deep learning can solve the above issues, the demand for a comprehensive dataset hampers its applicability in magnetic tracking. Thus, we propose an annular magnet pose estimation network (called AMagPoseNet) based on dual-domain few-shot learning from a prior mathematical model, which consists of two subnetworks: PoseNet and CaliNet. PoseNet learns to estimate the magnet pose from the prior mathematical model, and CaliNet is designed to narrow the gap between the mathematical model domain and the real-world domain. Experimental results reveal that the AMagPoseNet outperforms the optimization-based method regarding localization accuracy (1.87$\pm$1.14 mm, 1.89$\pm \text{0.81}^{\circ }$), robustness (nondependence on initial guesses), and computational latency (2.08$\pm$0.02 ms). In addition, the six-degree-of-freedom pose of the magnet could be estimated when discriminative magnetic field features are provided. With the assistance of the mathematical model, the AMagPoseNet requires only a few real-world samples and has excellent performance, showing great potential for practical biomedical and industrial applications. Shijian Su, Sishen Yuan, Mengya Xu, Huxin Gao, Xiaoxiao Yang, Hongliang Ren 0001 |
IEEE Trans. Ind. Informatics | 5 |
| 2022 | Few-shot Edge Classification in Graph Meta-learningabstractRecent few-shot learning methods based on graph neural networks (GNN) over-focus on the connections between nodes while ignoring the pair-wise relations between nodes. Meta-learning aims at model parameter initialization, enabling the model to gain the generalization capability, which assists GNN to pay more attention to nodes. There are rare methods to apply meta-learning to non-Euclidean spaces (such as graph structures). Thus, we propose a graph meta-learning framework, Meta Edge-labeling Graph Neural Network (Meta-EGNN), to solve image classification in few-shot learning. Meta-EGNN can learn a better parameter initialization for GNN with the prediction of edge labels, which can enhance the generalization of the model on unseen tasks. We also introduce the first-order gradient model-agnostic meta-learning into meta-EGNN, which can not only reduce the computational costs, but also help meta-EGNN extend to the transductive inference. The experimental results on two benchmarks prove that Meta-EGNN is competitive in both supervised and semi-supervised image classification. Xiaoxiao Yang, Jungang Xu |
DSAA | 1 |
| 2022 | BAANet: Learning Bi-directional Adaptive Attention Gates for Multispectral Pedestrian DetectionabstractThermal 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. Xiaoxiao Yang, Yeqiang Qian, Hui-Jie Zhu, Ming Yang 0002 |
ICRA | 1 |
| 2022 | GESRsim: Gastrointestinal Endoscopic Surgical Robot SimulatorabstractRobot-assisted gastrointestinal endoscopic surgery (GES) as a kind of natural orifice transluminal endoscopic surgery (NOTES) is the next-generation minimally invasive surgery (MIS). Besides, rendering certain autonomy to a Gas-trointestinal Endoscopic Surgical Robot (GESR) is promising but highly challenging. Therefore, to accelerate the development and augment the autonomy of GESR, we use CoppeliaSim to develop the first robotic simulator for the GESR system (GESRsim) based on our previous design. The GESRsim provides several 3D models and kinematics of our designed manipulators and endoscopic snake bone. Additionally, we build several scenes for robotic GES training and then utilize different programming interfaces to perform teleoperation. Furthermore, several advanced control algorithms, including visual servoing (VS) and deep reinforcement learning (DRL), are implemented to verify the performance of the GESRsim. Huxin Gao, Zedong Zhang, Xiao Xiao 0006, Liang Qiu 0002, Xiaoxiao Yang, Ruoyi Hao, Xiuli Zuo, Hongliang Ren 0001 |
IROS | 6 |
| 2021 | Photometric Stereo Based on Multiple Kernel Learning
Yu Guo 0006, Xiaoxiao Yang, Xuetao Zhang 0001, Fei Wang 0008 |
ICIG (3) | 3 |
| 2021 | Dynamic Hypergraph Regularized Broad Learning System for Image Classification
Xiaoxiao Yang, Yu Guo 0006, Peilin Jiang, Fei Wang 0008 |
ICIG (1) | 1 |
| 2021 | Online robust echo state broad learning system
Yu Guo 0006, Xiaoxiao Yang, Fei Wang 0008, Badong Chen |
Neurocomputing | 2 |
| 2020 | Learning Consistency Pursued Correlation Filters for Real-Time UAV TrackingabstractCorrelation 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 (~43FPS) on a single CPU. Changhong Fu 0001, Xiaoxiao Yang, Juntao Xu, Changjing Liu, Peng Lu 0003 |
IROS | 2 |
| 2018 | Branching Bisimulation and Concurrent Object VerificationabstractLinearizability and progress properties are key correctness notions for concurrent objects. This paper presents novel verification techniques for both property classes. The key of our techniques is based on the branching bisimulation equivalence. We first show that it suffices to check linearizability on the quotient object program under branching bisimulation. This is appealing, as it does not rely on linearization points. Further, by exploiting divergence-sensitive branching bisimilarity, our approach proves progress properties (e.g., lock-, wait-freedom) by comparing the concurrent to-be-verified object program against an abstract program consisting of atomic blocks. Our work thus enables the usage of well-known proof techniques for branching bisimulation to check the correctness of concurrent objects. The potential of our approach is illustrated by verifying linearizability and lock-freedom of 14 benchmark algorithms from the literature. Our experiments confirm one known bug and reveals one new bug. Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, Hao Wu 0013 |
DSN | 1 |
| 2017 | A Robust Hand Cursor Interaction Method Using KinectabstractIn this paper, we present a realtime natural interaction system by using Kinect sensor. It can stability and smoothly control hand like mouse by user's holding hands, and implement common mouse operations such as 'clicking', 'dragging' and 'dropping' so on. Our interaction system is made of several novel technique. It can identify the user's interaction with intent by detecting the engaged/disengaged gestures, and distinguish the primary user in the crowd, build a physical interaction zone to map the user's 3D hand position to 2D screen position in a timely and user-friendly manner. Our main contribution is to combine gesture recognition and gesture-tracking, and to implement an interaction application system with the details. Zhiwen Lei, Xiaoxiao Yang, Yanzhou Gong, Weixing Huang, Jian Wang 0029, Guigang Zhang |
ISM | 2 |
| 2016 | Performance Evaluation of Concurrent Data Structures
Hao Wu 0013, Xiaoxiao Yang, Joost-Pieter Katoen |
SETTA | 2 |
| 2014 | A temporal programming model with atomic blocks based on projection temporal logic
Xiaoxiao Yang, Yu Zhang 0086, Ming Fu, Xinyu Feng 0001 |
Frontiers Comput. Sci. | 1 |
| 2012 | A Concurrent Temporal Programming Model with Atomic Blocks
Xiaoxiao Yang, Yu Zhang 0086, Ming Fu, Xinyu Feng 0001 |
ICFEM | 1 |
| 2010 | Axiomatic Temporal Logic Programs VerificationabstractIn this paper, we investigate the axiomatic system of Modeling Simulation and Verification Language (MSVL). To this end, a set of state axioms and state inference rules is given. They are useful to deduce a program into its normal form. Further, a propositional projection temporal logic is used as assertion language to describe the required property of a program. Moreover, to deduce a program over an interval, a set of rules in terms of triple like Hoare logic is formalized. These rules enable us to deduce a program in its normal form at the current state to the next one and to verify safety, liveness properties over an interval. Xiaoxiao Yang |
TASE | 1 |
| 2010 | Axiomatic semantics of projection temporal logic programsabstractIn this paper, we investigate the axiomatic semantics of the projection temporal logic programming language MSVL. To this end, we employ Propositional Projection Temporal Logic (PPTL) as an assertion language to specify the desired properties. We give a set of state axioms and state inference rules. In order to deduce a program over an interval, we also formalise a set of rules in terms of a Hoare logic-like triple. These rules enable us to deduce a program into its normal form and from the current state to the next one. They also enable us to verify properties over intervals. In this way, an axiom system for proving the correctness of MSVL programs is established. The axiom system is proved to be sound and relatively complete with respect to an operational model of MSVL, and give an example showing how the axiom system works. Finally, we employ a recently developed prototype verifier based on PVS as an example of semi-automatic verification using MSVL. Xiaoxiao Yang |
Math. Struct. Comput. Sci. | 1 |
| 2008 | Framed temporal logic programming
Xiaoxiao Yang, Maciej Koutny |
Sci. Comput. Program. | 2 |
| 2007 | Operational Semantics of Framed Temporal Logic Programs
Xiaoxiao Yang |
SOFSEM (1) | 1 |
| 2007 | An Interpreter for Framed Tempura and Its ApplicationabstractThis paper discusses the implementation mechanism and its application of an interpreter for a framed temporal logic programming language called framed tempura. Firstly, the basic approach based on the normal form is presented. Then, the structure of the interpreter is illustrated and each of its modules is explained. The work flow of the reduction of programs is given in detail. In particular, the implementation approaches of several important new constructs including frame, await, projection, pointer are presented. As an application, the interpreter is used as a simulator of service models of OWL-S for the Web service composition. Yongtao Ma, Xiaoxiao Yang |
TASE | 4 |
| 2005 | Semantics of Framed Temporal Logic Programs
Xiaoxiao Yang, Maciej Koutny |
ICLP | 2 |