Author name cluster

Nan Zhang

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

36 papers

2 author rows

EAAI Journal 2026 Journal Article

Graph channel receptive field transformer for multi-agent trajectory prediction

Jiankun Peng
Jiakang Wang
Nan Zhang
Di Wu
Chunye Ma

Multi-agent trajectory prediction is critical for safe autonomous driving. However, existing vectorized methods face limitations in modeling local interactions and capturing global dependencies, struggling with interaction uncertainties and long-range dependencies in complex traffic. To address these challenges, we propose Graph Channel-Receptive Field Transformer (GCRFormer). The framework models the traffic scene as a heterogeneous graph to uniformly represent agent trajectories and map features. It integrates a Graph Channel Weight Tuning (GCWT) mechanism to aggregate local interactions and lane constraints. By combining GCWT with a Dilated Graph Receptive Field (DGRF) module, it captures long-range dependencies and generates multimodal candidate embeddings. A decoder then fuses these hierarchical features to output future trajectories and their associated probabilities for all agents. Experiments conducted on the Argoverse1 benchmark confirm that the proposed GCRFormer architecture outperforms existing state-of-the-art methods, showcasing its enhanced capability in modeling complex interactions for accurate trajectory prediction.

EAAI Journal 2026 Journal Article

Rethinking the local constraints: Geometric continuity regularization for image alignment

Yinqi Chen
Yangting Zheng
Peiwen Li
Weijian Luo
Shuo Kang
Xiang Gao
Chao Liu
Shuo Zhang

In image alignment, existing studies frequently neglect the modeling of featureless areas where reliable features are inherently absent. While indirect strategies, such as adding more geometric features, have been used to reduce such regions, they are limited by the natural variability of scenes. Instead, directly modeling these areas allows local consistency constraints to propagate transformations from feature-rich to featureless regions. However, existing local consistency constraints rely solely on parametric continuity (C1), which can cause excessive smoothness and distortion due to the excessive constraints on parameters. In contrast, geometric continuity (G1) relaxes parameter constraints and ensures visual accuracy, leading to results with lower distorted energy. Thus, this paper, for the first time, rigorously examines the rationale of local constraints, validates their capacity for featureless-region modeling, and theoretically demonstrates that G1 continuity effectively minimizes distortion. Building on these analyses, we introduce G1 continuity regularization; to enforce this property, the regularization term directly penalizes deviations from collinearity at mesh vertices or within network-learned transformations. Compared with existing approaches, our method achieves markedly superior performance.

AAAI Conference 2026 Conference Paper

Vista: Scene-Aware Optimization for Streaming Video Question Answering Under Post-Hoc Queries

Haocheng Lu
Nan Zhang
Wei Tao
Xiaoyang Qu
Guokuan Li
Jiguang Wan
Jianzong Wang

Streaming video question answering (Streaming Video QA) poses distinct challenges for multimodal large language models (MLLMs), as video frames arrive sequentially and user queries can be issued at arbitrary timepoints. Existing solutions relying on fixed-size memory or naive compression often suffer from context loss or memory overflow, limiting their effectiveness in long-form, real-time scenarios.We present Vista, a novel framework for scene-aware streaming video QA that enables efficient and scalable reasoning over continuous video streams. The innovation of Vista can be summarized in three aspects: (1) Scene-aware segmentation. Vista dynamically clusters incoming frames into temporally and visually coherent scene units. (2) Scene-aware compression. Each scene is compressed into a compact token representation and stored in GPU memory for efficient index-based retrieval, while the full-resolution frames are offloaded to CPU memory. (3) Scene-aware recall. Upon receiving a question, relevant scenes are selectively recalled and reintegrated into the model’s input space, enabling both efficiency and completeness. Vista is model-agnostic and integrates seamlessly with a variety of vision-language backbones, enabling long-context reasoning without compromising latency or memory efficiency. Extensive experiments on StreamingBench demonstrate that Vista achieves state-of-the-art performance, establishing a strong baseline for real-world streaming video understanding.

PDF Details DOI

TCS Journal 2025 Journal Article

Improved SARSA and DQN algorithms for reinforcement learning

Guangyu Yao
Nan Zhang
Zhenhua Duan
Cong Tian

Reinforcement learning is a branch of machine learning in which an agent interacts with an environment to learn optimal actions that maximize cumulative rewards. This paper aims to enhance the SARSA and DQN algorithms in four key aspects: the ε-greedy policy, reward function, value iteration approach, and sampling probability. The experiments are conducted in three scenarios: path planning, CartPole, and MountainCar. The results show that, in these environments, the improved algorithms exhibit better convergence, higher rewards, and more stable training processes.

NeurIPS Conference 2025 Conference Paper

Mamba Only Glances Once (MOGO): A Lightweight Framework for Efficient Video Action Detection

Yunqing Liu
Nan Zhang
Fangjun Wang
Kengo Murata
Takuma Yamamoto
Osafumi Nakayama
Genta Suzuki
Zhiming Tan

Mamba, a lightweight sequence modeling framework offering near-linear complexity, presents a promising alternative to Transformers. In this work, we introduce MOGO (Mamba Only Glances Once), an end-to-end framework for efficient video action detection built entirely on the Mamba architecture. In MOGO, our newly designed Mamba-based decoder can even use just one Mamba layer to effectively perform action detection. It uses neither Transformer structures nor RCNN-like methods for proposal detection. Our framework introduces two key innovations. First, we propose a pure Mamba-based encoder-decoder architecture. The encoder processes cross-frame video information, while the decoder incorporates two novel Mamba-based structures that leverage Mamba’s intrinsic capabilities to detect actions. Theoretical analysis and ablation experiments confirm their synergy and the necessity of each structure. Second, we design a video token construction mechanism to improve the model's performance. The token importance block can ensure that the retained token information is highly relevant to the predicted targets. These two innovations make MOGO both efficient and accurate, as demonstrated on the JHMDB and UCF101-24 benchmark datasets. Compared to SOTA action detection methods, MOGO achieves superior performance in terms of GFLOPs, model parameters, and inference speed (latency) with comparable detection precision. Additionally, it requires significantly less GPU memory than some SOTA token reconstruction methods. Code is available at https: //github. com/YunqingLiu-ML/MOGO.

AAAI Conference 2025 Conference Paper

Point Cloud Semantic Segmentation with Sparse and Inhomogeneous Annotations

Zhiyi Pan
Nan Zhang
Wei Gao
Shan Liu
Ge Li

Utilizing uniformly distributed sparse annotations, weakly supervised learning alleviates the heavy reliance on fine-grained annotations in point cloud semantic segmentation tasks. However, few works discuss the inhomogeneity of sparse annotations, albeit it is common in real-world scenarios. Therefore, this work introduces the probability density function into the gradient sampling approximation method to qualitatively analyze the impact of annotation sparsity and inhomogeneity under weakly supervised learning. Based on our analysis, we propose an Adaptive Annotation Distribution Network (AADNet) capable of robust learning on arbitrarily distributed sparse annotations. Specifically, we propose a label-aware point cloud downsampling strategy to increase the proportion of annotations involved in the training stage. Furthermore, we design the multiplicative dynamic entropy as the gradient calibration function to mitigate the gradient bias caused by non-uniformly distributed sparse annotations and explicitly reduce the epistemic uncertainty. Without any prior restrictions and additional information, our proposed method achieves comprehensive performance improvements at multiple label rates and different annotation distributions.

PDF Details DOI

TCS Journal 2025 Journal Article

SAT-based bounded model checking for propositional projection temporal logic

Zhenhua Duan
Cong Tian
Nan Zhang
Chaofeng Yu
Mengfei Yang
Jia He

This paper presents a bounded model checking (BMC) approach for propositional projection temporal logic (PPTL). To this end, first PPTL is briefly introduced. Then, bounded semantics of PPTL is defined according to its semantics in logic theory. Further, a reduction method from BMC to SAT is given in detail. In addition, an example is presented to illustrate how the approach works. Finally, miniSAT is employed to solve the SAT based BMC problem by means of verifying RMS algorithm in detail. Our experience shows that SAT based BMC approach for PPTL proposed in the paper is useful and feasible.

ICLR Conference 2025 Conference Paper

SiReRAG: Indexing Similar and Related Information for Multihop Reasoning

Nan Zhang
Prafulla Kumar Choubey
Alexander R. Fabbri
Gabriel Bernadett-Shapiro
Rui Zhang 0037
Prasenjit Mitra
Caiming Xiong
Chien-Sheng Wu

Indexing is an important step towards strong performance in retrieval-augmented generation (RAG) systems. However, existing methods organize data based on either semantic similarity (similarity) or related information (relatedness), but do not cover both perspectives comprehensively. Our analysis reveals that modeling only one perspective results in insufficient knowledge synthesis, leading to suboptimal performance on complex tasks requiring multihop reasoning. In this paper, we propose SiReRAG, a novel RAG indexing approach that explicitly considers both similar and related information. On the similarity side, we follow existing work and explore some variances to construct a similarity tree based on recursive summarization. On the relatedness side, SiReRAG extracts propositions and entities from texts, groups propositions via shared entities, and generates recursive summaries to construct a relatedness tree. We index and flatten both similarity and relatedness trees into a unified retrieval pool. Our experiments demonstrate that SiReRAG consistently outperforms state-of-the-art indexing methods on three multihop datasets (MuSiQue, 2WikiMultiHopQA, and HotpotQA), with an average 1.9% improvement in F1 scores. As a reasonably efficient solution, SiReRAG enhances existing reranking methods significantly, with up to 7.8% improvement in average F1 scores. Our code is available at https://github.com/SalesforceAIResearch/SiReRAG.

UAI Conference 2024 Conference Paper

Bias-aware Boolean Matrix Factorization Using Disentangled Representation Learning

Xiao Wang 0099
Jia Wang
Tong Zhao 0002
Yijie Wang
Nan Zhang
Yong Zang
Sha Cao
Chi Zhang 0021

Boolean matrix factorization (BMF) has been widely utilized in fields such as recommendation systems, graph learning, text mining, and -omics data analysis. Traditional BMF methods decompose a binary matrix into the Boolean product of two lower-rank Boolean matrices plus homoscedastic random errors. However, real-world binary data typically involves biases arising from heterogeneous row- and column-wise signal distributions. Such biases can lead to suboptimal fitting and unexplainable predictions if not accounted for. In this study, we reconceptualize the binary data generation as the Boolean sum of three components: a binary pattern matrix, a background bias matrix influenced by heterogeneous row or column distributions, and random flipping errors. We introduce a novel Disentangled Representation Learning for Binary matrices (DRLB) method, which employs a dual auto-encoder network to reveal the true patterns. DRLB can be seamlessly integrated with existing BMF techniques to facilitate bias-aware BMF. Our experiments with both synthetic and real-world datasets show that DRLB significantly enhances the precision of traditional BMF methods while offering high scalability. Moreover, the bias matrix detected by DRLB accurately reflects the inherent biases in synthetic data, and the patterns identified in the bias-corrected real-world data exhibit enhanced interpretability.

YNICL Journal 2024 Journal Article

Dysregulated cerebral blood flow, rather than gray matter Volume, exhibits stronger correlations with blood inflammatory and lipid markers in depression

Lijun Kang
Wei Wang
Zhaowen Nie
Qian Gong
Lihua Yao
Dan Xiang
Nan Zhang
Ning Tu

Arterial spin labeling (ASL) can be used to detect differences in perfusion for multiple brain regions thought to be important in major depressive disorder (MDD). However, the potential of cerebral blood flow (CBF) to predict MDD and its correlations between the blood lipid levels and immune markers, which are closely related to MDD and brain function change, remain unclear. The 451 individuals - 298 with MDD and 133 healthy controls who underwent MRI at a single time point with arterial spin labelling and a high resolution T1-weighted structural scan. A proportion of MDD also provided blood samples for analysis of lipid and immune markers. We performed CBF case-control comparisons, random forest model construction, and exploratory correlation analyses. Moreover, we investigated the relationship between gray matter volume (GMV), blood lipids, and the immune system within the same sample to assess the differences in CBF and GMV. We found that the left inferior parietal but supramarginal and angular gyrus were significantly different between the MDD patients and HCs (voxel-wise P < 0.001, cluster-wise FWE correction). And bilateral inferior temporal (ITG), right middle temporal gyrus and left precentral gyrus CBF predict MDD (the area under the receiver operating characteristic curve of the random forest model is 0.717) and that CBF is a more sensitive predictor of MDD than GMV. The left ITG showed a positive correlation trend with immunoglobulin G (r = 0.260) and CD4 counts (r = 0.283). The right ITG showed a correlation trend with Total Cholesterol (r = -0.249) and tumour necrosis factor-alpha (r = -0.295). Immunity and lipids were closely related to CBF change, with the immunity relationship potentially playing a greater role. The interactions between CBF, plasma lipids and immune index could therefore represent an MDD pathophysiological mechanism. The current findings provide evidence for targeted regulation of CBF or immune properties in MDD.

TCS Journal 2024 Journal Article

Generating Java code pairing with ChatGPT

Zelong Zhao
Nan Zhang
Bin Yu
Zhenhua Duan

The Large Language Models (LLMs) like ChatGPT 3. 5 have created a new era of automatic code generation. However, the existing research primarily focuses on generating simple code based on datasets (such as HumanEval, etc.). Most of approaches pay less attention to complex and practical code generation. Therefore, in this paper, we propose a new approach called “Xd-CodeGen” which can be used to generate large scale Java code. This approach is composed of four phases: requirement analysis, modeling, code generation, and code verification. In the requirement analysis phase, ChatGPT 3. 5 is utilized to decompose and restate user requirements. To do so, a knowledge graph is developed to describe entities and their relationship in detail. Further, Propositional Projection Temporal Logic (PPTL) formulas are employed to define the properties of requirements. In the modeling phase, we use knowledge graphs to enhance prompts and generate UML class and activity diagrams for each sub-requirement using ChatGPT 3. 5. In the code generation phase, based on established UML models, we make use of prompt engineering and knowledge graph to generate Java code. In the code verification phase, a runtime verification at code level approach is employed to verify generated Java code. Finally, we apply the proposed approach to develop a practical Java web project.

AAAI Conference 2024 Conference Paper

Less Is More: Label Recommendation for Weakly Supervised Point Cloud Semantic Segmentation

Zhiyi Pan
Nan Zhang
Wei Gao
Shan Liu
Ge Li

Weak supervision has proven to be an effective strategy for reducing the burden of annotating semantic segmentation tasks in 3D space. However, unconstrained or heuristic weakly supervised annotation forms may lead to suboptimal label efficiency. To address this issue, we propose a novel label recommendation framework for weakly supervised point cloud semantic segmentation. Distinct from pre-training and active learning, the label recommendation framework consists of three stages: inductive bias learning, recommendations for points to be labeled, and point cloud semantic segmentation learning. In practice, we first introduce the point cloud upsampling task to induct inductive bias from structural information. During the recommendation stage, we present a cross-scene clustering strategy to generate centers of clustering as recommended points. Then we introduce a recommended point positions attention module LabelAttention to model the long-range dependency under sparse annotations. Additionally, we employ position encoding to enhance the spatial awareness of semantic features. Throughout the framework, the useful information obtained from inductive bias learning is propagated to subsequent semantic segmentation networks in the form of label positions. Experimental results demonstrate that our framework outperforms weakly supervised point cloud semantic segmentation methods and other methods for labeling efficiency on S3DIS and ScanNetV2, even at an extremely low label rate.

PDF Details DOI

EAAI Journal 2024 Journal Article

Mgformer: Multi-group transformer for multivariate time series classification

Jianfeng Wen
Nan Zhang
Xuzhe Lu
Zhongyi Hu
Hui Huang

Multivariate time series classification (MTSC) is a crucial task in data science, providing a foundation for analyzing and predicting complex, multi-dimensional data patterns. However, traditional MTSC methods are challenging to handle high-dimensional data effectively and necessitate complex feature engineering. Although deep learning methods have shown excellent performance in handling high-dimensional data, they have difficulty learning diverse temporal patterns in multivariate time series (MTS) and fail to capture deep channel-wise correlations. To this end, we propose a novel MTSC model based on Transformers named Mgformer, which has two basic structures, i. e. , the multi-group Transformer module and the channel attention mask module. The multi-group Transformer module combines temporal patching and multiple groups of Transformers to learn complex with diverse temporal patterns at different scales. An attention masking strategy is employed by the channel attention mask module to improve the model’s capacity to learn channel-wise correlations and decrease information loss during training. Experimental results on 27 benchmark MTS datasets show that Mgformer is better than state-of-the-art MTSC methods.

TCS Journal 2023 Journal Article

A proof system for unified temporal logic

Nan Zhang
Chaofeng Yu
Zhenhua Duan
Cong Tian

Unified Temporal Logic (UTL) combines all characteristics of traditional Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). It can be used to describe full regular and omega-regular properties, which are often encountered in the field of formal verification. To support formal verification with UTL, this paper proposes a proof system for UTL. First, the syntax and semantics of UTL are briefly introduced. Further, axioms and inference rules are formalized. Besides, a number of theorems are derived and proved to refine the system. Moreover, the soundness and completeness of the proof system are proved in detail. To facilitate the completeness proof, some auxiliary lemmas are introduced and proved in advance. Finally, an example is given to illustrate how to use this proof system for verifying properties of a system.

IJCAI Conference 2023 Conference Paper

Null-Space Diffusion Sampling for Zero-Shot Point Cloud Completion

Xinhua Cheng
Nan Zhang
Jiwen Yu
Yinhuai Wang
Ge Li
Jian Zhang

Point cloud completion aims at estimating the complete data of objects from degraded observations. Despite existing completion methods achieving impressive performances, they rely heavily on degraded-complete data pairs for supervision. In this work, we propose a novel framework named Null-Space Diffusion Sampling (NSDS) to solve the point cloud completion task in a zero-shot manner. By leveraging a pre-trained point cloud diffusion model as the off-the-shelf generator, our sampling approach can generate desired completion outputs with the guidance of the observed degraded data without any extra training. Furthermore, we propose a tolerant loop mechanism to improve the quality of completion results for hard cases. Experimental results demonstrate our zero-shot framework achieves superior completion performance than unsupervised methods and comparable performance to supervised methods in various degraded situations.

PDF Details DOI

TCS Journal 2022 Journal Article

PPTL specification mining based on LNFG

Xinya Ning
Nan Zhang
Zhenhua Duan
Cong Tian

A formal specification is a formal description of system requirements, which is a necessity for formal verification. Due to various reasons, some systems lack of formal specifications. Compared with CTL and LTL, Propositional Projection Temporal Logic (PPTL) has a full regular expressive power. Accordingly, a pattern-library-based PPTL specification mining tool PPTLMiner [1] is able to dig out a better expression of system specification. However, there's still some room for improvement in PPTLMiner, such as deep recursion, high time complexity and space complexity, which limit the use of PPTLMiner in practical applications. Therefore, in this paper, a new PPTL specification mining approach based on Labeled Normal Form Graph (LNFG) is proposed and a supporting tool PPTLMiner+ is also developed. Finally, a specification mining example using PPTLMiner+ is given to illustrate the effectiveness and practicality of the new approach. In this example, a typical algorithm in Swarm Intelligence-Bee Colony Algorithm is selected as a target program, and the working order of EmployedBees, OnlookerBees and ScoutBees is obtained using PPTLMiner+. Further, PPTLMiner+ is compared with PPTLMiner as well as the classical linear specification mining tool Texada [2, 3] in terms of time and memory to illustrate the effectiveness and practicability of the proposed method.

TCS Journal 2021 Journal Article

Temporal logic specification mining of programs

Nan Zhang
Bin Yu
Cong Tian
Zhenhua Duan
Xiaoshuai Yuan

This paper proposes a dynamic approach of specification mining for Propositional Projection Temporal Logic (PPTL). To this end, a pattern library is built to collect some common temporal relation among events. Further, several algorithms of specification mining for PPTL are designed. With our approach, PPTL specifications are mined from a trace set of a target program by using patterns in the library. In addition, a specification mining tool PPTLMiner supporting this approach is developed. In practice, given a trace set and user selected patterns, PPTLMiner can capture PPTL specifications of target programs.

TCS Journal 2021 Journal Article

Unified temporal logic

Nan Zhang
Zhenhua Duan
Cong Tian

This paper proposes a new temporal logic named Unified Temporal Logic (UTL). First, the syntax and semantics of UTL are inductively defined. Further, logic laws in UTL are formalized and proved. Moreover, the normal forms of UTL formulas are defined and proved. To illustrate how to describe properties with UTL, an example of an elevator control system is given. In general, UTL combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). So properties involving the “until” construct in LTL and the “chop” construct in PPTL can easily be represented in UTL. In addition, both finite and infinite models (intervals) are supported. With UTL, we are able to specify and verify some practical properties which cannot easily be formalized in LTL and PPTL.

TCS Journal 2020 Journal Article

A novel approach to verifying context free properties of programs

Nan Zhang
Zhenhua Duan
Cong Tian
Hongwei Du

This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m ′. Then program m and formula ¬ m ′ are interpreted by means of executing programs m and m ′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.

TCS Journal 2020 Journal Article

A sound and complete proof system for a unified temporal logic

Liang Zhao
Xiaobing Wang
Xinfeng Shu
Nan Zhang

Theorem proving is one of the most widely used approaches to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a sound and complete proof system for Propositional Projection Temporal Logic (PPTL) with indexed expressions, which is a unified temporal logic that subsumes the well used Linear Temporal Logic (LTL). First, the syntax, semantics and logic laws of PPTL that allows indexed expressions are introduced, and the representation of LTL constructs by PPTL formulas is illustrated. Then, the proof system for the logic is presented which consists of axioms and inference rules for the derivation of both basic constructs and indexed expressions. To show the capability of the proof system, several examples of formal proofs are provided. Finally, the soundness and completeness of the proof system are demonstrated.

TCS Journal 2020 Journal Article

Efficient decision procedure for propositional projection temporal logic

Xinfeng Shu
Nan Zhang
Xiaobing Wang
Liang Zhao

The decision problem for Propositional Projection Temporal Logic (PPTL) has been solved successfully, however time complexity of the procedure is increased exponentially to the length of the formula. To solve the problem, a labeled unified complete normal form is introduced as the intermediate form to rewrite a PPTL formula into its equivalent labeled normal form, based on which the labeled normal form graph is constructed, and an efficient decision procedure for PPTL is formalized with the time complexity linear to the length of the formula and the size of the power set of the atomic propositions in the formula. Besides, an example is given to show how the improved decision procedure works.

TCS Journal 2020 Journal Article

Translating Xd-C programs to MSVL programs

Meng Wang
Cong Tian
Nan Zhang
Zhenhua Duan
Chenguang Yao

C language is one of the most popular languages for software systems. In order to verify safety, reliability and security properties of such systems written in C, a tool UMC4M for runtime verification at code level based on Modeling, Simulation and Verification Language (MSVL) and its compiler MC is employed. To do so, a C program P has to be translated to an MSVL program M and the negation of a desired property Q is also translated to an MSVL program M', then “M and M'” is compiled and executed armed with MC. Whether P violates Q is checked by evaluating whether there exists an acceptable execution of new MSVL program “M and M'”. Therefore, how to translate a C program to an MSVL program is a critical issue. However, in general, C is of complicated structures with goto statement. In this paper, we confine the syntax of C in a suitable subset called Xd-C without loss of expressiveness. Further, we present a translation algorithm from an Xd-C program to an MSVL program based on translation algorithms for expressions and statements. Moreover, the equivalences between expressions and statements involved in Xd-C and MSVL programs are inductively proved. Subsequently, the equivalence between the original Xd-C program and the translated MSVL program is also proved. In addition, the proposed approach has been implemented by a tool called C 2 M. A benchmark of experiments including 13 real-world Xd-C programs is conducted. The results show that C 2 M works effectively.

TCS Journal 2019 Journal Article

Index set expressions can represent temporal logic formulas

Zhenhua Duan
Cong Tian
Nan Zhang
Qian Ma
Hongwei Du

In Temporal Logic (TL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions, are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed since their equivalent concise syntax formulas can be found. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax by means of fixed-point approach. Firstly, we present two kinds of formulas, namely ⋁ i ∈ N 0 ◯ i Q and ⋁ i ∈ N 0 Q i, and prove they are indeed well-formed by proving they are equivalent to formulas ◇Q and Q ⁎ respectively. Further, we generalize ⋁ i ∈ N 0 ◯ i Q to ⋁ i ∈ N 0 P ( i ) ∧ ◯ i Q and explore the least and greatest fixed-points of an abstract equation X ≡ Q ∨ P ∧ ◯ X. Based on these, some well-formed special instances of ⋁ i ∈ N 0 P ( i ) ∧ ◯ i Q are obtained. Besides, with the index set expression technique, we equivalently represent ‘ U ’ (strong until) and ‘ W ’ (weak until) constructs of propositional Linear Temporal Logic (LTL) within Propositional Projection Temporal Logic (PPTL).

YNICL Journal 2019 Journal Article

Resting-state functional connectivity predicts individual language impairment of patients with left hemispheric gliomas involving language network

Binke Yuan
Nan Zhang
Jing Yan
Jingliang Cheng
Junfeng Lu
Jinsong Wu

Language deficits following brain tumors should consider the dynamic interactions between different tumor growth kinetics and functional network reorganization. We measured the resting-state functional connectivity of 126 patients with left cerebral gliomas involving language network areas, including 77 patients with low-grade gliomas (LGG) and 49 patients with high-grade gliomas (HGG). Functional network mapping for language was performed by construction of a multivariate machine learning-based prediction model of individual aphasia quotient (AQ), a summary score that indicates overall severity of language impairment. We found that the AQ scores for HGG patients were significantly lower than those of LGG patients. The prediction accuracy of HGG patients (R2 = 0. 27, permutation P = 0. 007) was much higher than that of LGG patients (R2 = 0. 09, permutation P = 0. 032). The rsFC regions predictive of LGG's AQ involved the bilateral frontal, temporal, and parietal lobes, subcortical regions, and bilateral cerebro-cerebellar connections, mainly in regions belonging to the canonical language network. The functional network of language processing for HGG patients showed strong dependence on connections of the left cerebro-cerebellar connections, limbic system, and the temporal, occipital, and prefrontal lobes. Together, our findings suggested that individual language processing of glioma patients links large-scale, bilateral, cortico-subcortical, and cerebro-cerebellar functional networks with different network reorganizational mechanisms underlying the different levels of language impairments in LGG and HGG patients.

TCS Journal 2018 Journal Article

A compiler for MSVL and its applications

Kai Yang
Zhenhua Duan
Cong Tian
Nan Zhang

In this paper, we present a method for implementing a compiler called MC for Modeling, Simulation and Verification Language (MSVL) based on LLVM. MC accepts a well formed MSVL program as input and generates an executable binary code. Different from other compilers, MC can be used not only to compile programs but also to model and verify programs. The details of implementation including the architecture design, lexical, syntactic and semantic analysis, as well as preprocessing and scheduling algorithms. Besides, we show MC can be utilized as an infrastructure for Artificial Intelligence (AI) planning. Several examples are given to show applications of MC in modeling and verifying programs, as well as AI planning.

EAAI Journal 2018 Journal Article

An evolving T–S fuzzy model identification approach based on a special membership function and its application on pump-turbine governing system

Chaoshun Li
Wen Zou
Nan Zhang
Xinjie Lai

Hyper-plane-shaped clustering (HPSC) has been proved to be more effective in Takagi–Sugeno (T–S) fuzzy model identification compared with hyper-sphere-shaped clustering (HSSC). However, there is no special membership function matching HPSC in fuzzy modeling, and the commonly used bell-shaped Gaussian function is more suitable for HSSC. In this paper, a novel T–S fuzzy model identification method is adopted, in which a new fuzzy membership function designed for HSPC is designed. In this approach, a fuzzy c-regression model based clustering method is used to partition the fuzzy space firstly; and then a new HPSC fuzzy membership function is designed to identify the antecedent membership function (MF) parameters; finally the gravitational search algorithm is applied to optimize the MF parameters further. Experimental results on several benchmark problems show that modeling accuracies have been promoted significantly. The proposed approach has been applied in fuzzy modeling of pump-turbine governing system (PTGS). The comparative experimental results reveal that the proposed approach could achieve high accuracy and would be an effective modeling tool for complicated nonlinear system in engineering applications.

ICRA Conference 2018 Conference Paper

Learning Place-and-Time-Dependent Binary Descriptors for Long-Term Visual Localization

Nan Zhang
Michael Warren
Tim D. Barfoot

Vision-based navigation is extremely susceptible to natural scene changes. This can result in localization failures in less than a few hours after map creation. To combat short-term illumination changes as well as long-term seasonal variations, we propose using a place-and-time-dependent binary descriptor that adapts to different scenarios in an online fashion. This is achieved by extending the GRIEF [6] evolution algorithm in two ways: correspondence generation using a known pose change and the inclusion of LATCH triplets in addition to BRIEF comparisons for descriptor generation. We show the adaptive descriptor outperforms a single descriptor scheme for localization within a single-experience Visual Teach and Repeat (VT&R) system while maintaining the efficiency of binary descriptors. By adapting the description function to different environmental conditions, it allows the system to operate for a longer period before a new experience is required. In the presence of extreme illumination changes from day to night, we obtain 40% more inlier matches compared to SURF. In the case of seasonal variations, a 70% increase is demonstrated. The increased correspondences result in more localizable sections along the paths, amounting to a 25% and 150% increase in the lighting and seasonal cases, respectively.

TCS Journal 2016 Journal Article

A canonical form based decision procedure and model checking approach for propositional projection temporal logic

Zhenhua Duan
Cong Tian
Nan Zhang

This paper proposes a Canonical Form (CF) for chop formulas of Propositional Projection Temporal Logic (PPTL). Based on CF, an improved algorithm for constructing Labeled Normal Form Graph (LNFG) of a PPTL formula is presented. This improvement leads to a better decision procedure for PPTL with infinite models. In addition, a transformation from LNFGs to Generalized Büchi Automata (GBA) and then Büchi Automata (BA) is formalized. Thus, a SPIN based model checking approach is generalized for PPTL. To illustrate how these algorithms work, several examples are given.

TCS Journal 2016 Journal Article

A complete axiom system for propositional projection temporal logic with cylinder computation model

Nan Zhang
Zhenhua Duan
Cong Tian

To specify and verify multi-core parallel programs in a uniform framework, this paper proposes an axiom system for CCM–PPTL which extends that of PPTL by including transformation rules for sequence expressions and axioms as well as inference rules on the CCM construct. Further, the soundness and completeness of the extended axiom system are proved.

TCS Journal 2016 Journal Article

A mechanism of function calls in MSVL

Nan Zhang
Zhenhua Duan
Cong Tian

Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and internal function calls. To do so, the syntax of function definitions and function calls is formalized. Then, the syntax of expressions in MSVL is extended by including function calls. Further, the evaluation rules are redefined. Moreover, the set of statements in MSVL is also extended and the semantics of function call statements is formalized. In addition, the existence of minimal models of MSVL programs involving new added statements is proved. Finally, an example is given to illustrate how to interpret function calls in practice with MSVL.

EAAI Journal 2016 Journal Article

Parameter identification of a nonlinear model of hydraulic turbine governing system with an elastic water hammer based on a modified gravitational search algorithm

Chaoshun Li
Li Chang
Zhengjun Huang
Yi Liu
Nan Zhang

The hydraulic turbine governing system (HTGS) is a crucial control system of hydroelectric generating units (HGUs). Parameter identification of HTGS is an important issue for the modeling and control of HGUs. The parameter identification problem of HTGS is more difficult if the elastic water hammer model is considered in the system, and existing algorithms are not effective to solve it. To solve this new problem, a modified gravitational search algorithm (MGSA) has been proposed in which modifications have been made to improve the performance of the GSA from two aspects. First, the constant attenuation factor is replaced by a hyperbolic function to generate a better gravitational constant to balance the global exploration and local exploitation during different searching stages. Second, agent mutation is introduced to increase the diversity of agents and to strengthen the ability to jump out of the local minima of the GSA. The performance of the MGSA has been verified by 13 typical benchmark problems, and the experimental results and statistical analysis demonstrate that the proposed MGSA significantly outperforms the standard GSA and some other popular optimization algorithms. The MGSA is then employed in the parameter identification of a nonlinear model of HTGS with an elastic water hammer, and the experimental results indicate that MGSA locates more precise parameter values than the compared methods.

TCS Journal 2014 Journal Article

A formal proof of the deadline driven scheduler in PPTL axiomatic system

Nan Zhang
Zhenhua Duan
Cong Tian
Dingzhu Du

This paper presents an approach for verifying the correctness of the feasibility theorem on the deadline driven scheduler (DDS) with the axiom system of Propositional Projection Temporal Logic (PPTL). To do so, the deadline driven scheduling algorithm is modeled by an MSVL (Modeling, Simulation and Verification Language) program and the feasibility theorem is formulated by PPTL formulas with two parts: a necessary part and a sufficient part. Then, several lemmas are abstracted and proved by means of the axiom system of PPTL. With the help of the lemmas, two parts of the theorem are deduced respectively. This case study convinces us that some real-time properties of systems can be formally verified by theorem proving using the axiom system of PPTL.

TCS Journal 2013 Journal Article

A complete proof system for propositional projection temporal logic

Zhenhua Duan
Nan Zhang
Maciej Koutny

The paper presents a proof system for Propositional Projection Temporal Logic (PPTL) with projection-plus. The syntax, semantics, and logical laws of PPTL are introduced together with an axiom system consisting of axioms and inference rules. To facilitate proofs, some of the frequently used theorems are proved. A normal form of PPTL formulas is presented, and the soundness and completeness of the proof system are demonstrated. To show how the axiom system works, a full omega regular property for the mutual exclusion problem is specified by a PPTL formula and then a deductive proof of the property is performed.

TCS Journal 2013 Journal Article

A cylinder computation model for many-core parallel computing

Nan Zhang
Zhenhua Duan
Cong Tian

Many-core parallel computing and programming are new challenges to formal specification and verification. This paper presents a semantic model for many-core parallel computing systems so that the systems can be modeled and verified in a manageable way. The model is called Cylinder Computation Model (CCM) which is based on projection constructs in Projection Temporal Logic (PTL) and Modeling, Simulation and Verification Language (MSVL). To this end, the syntax and semantics of CCM are presented in detail. Further, some logic laws regarding CCM are given and the normal form of CCM programs is formalized and proved. Moreover, the operational semantics of CCM and an algorithm for implementing CCM programs within MSVL are also demonstrated. Finally, an example, simple word processor, is given to show how CCM works under MSVL paradigm.

TCS Journal 2012 Journal Article

An efficient approach for abstraction-refinement in model checking

Cong Tian
Zhenhua Duan
Nan Zhang

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In an abstract model, the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. Accordingly, the abstract model needs to be further refined where an NP-hard state separation problem is often involved. In this paper, a novel approach is presented, in which extra boolean variables are added to the abstract model for the refinement. With this approach, not only the NP-hard state separation problem can be avoided, but also a smaller refined abstract model can be obtained.

IS Journal 2008 Journal Article

DynaCAS: Computational Experiments and Decision Support for ITS

Nan Zhang
Fei-Yue Wang
Fenghua Zhu
Dongbin Zhao
Shuming Tang

Accurate, reliable, and timely traffic information is critical for deployment and operation of intelligent transportation systems (ITSs). Traffic forecasting for travelers and traffic operators should become at least as useful and convenient as weather reports. In the US, the Federal Highway Administration (FHWA) has envisioned a real-time traffic estimation and prediction system (TrEPS) as an ITS support platform that resides at traffic management centers (TMCs) for dynamic route assignment (DRA) and other transportation operations.