Researcher profile

Xiang Yin

Xiang Yin contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
21works
0followers
11topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

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

Published work

21 published item(s)

preprint2026arXiv

Evaluating the Utility of Personal Health Records in Personalized Health AI

Patient-managed Personal Health Records (PHRs) promises to empower patients to better understand their health; but information in the record is complex, potentially hindering insights. In this study, we assess the potential of large language models (LLMs, Gemini 3.0 Flash) to provide helpful answers to user health queries, when provided clinical data from PHRs as context. A total of 2,257 user queries were drawn from 3 different distributions to represent patient questions: shorter web search queries, longer questions derived from templates of chatbot conversations, and questions patients asked to their healthcare team (patient calls). Queries were matched with de-identified PHRs (from a pool of 1,945). Gemini responses were generated (1) without PHR context; (2) with a basic summary of demographics, conditions, and medications; (3) with full, extensive clinical notes. For evaluation, we leveraged an existing rating framework (SHARP), and developed a new framework for specific error modes when interpreting PHRs. Evaluation was performed using autoraters for the full set, and with clinician ratings for a subset (n=95), with both sets of raters knowing the full PHR context. We see significant improvements in the helpfulness of answers to all question types with PHR data (p < 0.001, paired t-test). We also observe potential gains in safety, accuracy, relevance and personalization of answers. Our PHR evaluation framework further identifies gaps in LLM understanding of particular aspects of complex PHRs, such as temporal disorientation, and rare but meaningful confabulations. These results suggest potential for PHR data to help people with a wide range of user needs; and provide a framework for monitoring for gaps in LLM answers based on PHR context. This study motivates further work to assess and realize potential benefits to users from understanding their health records.

preprint2026arXiv

On the Computation and Approximation of Backward Reachable Sets for Max-Plus Linear Systems using Polyhedras

This paper investigates reachability analysis for max-plus linear systems (MPLS), an important class of dynamical systems that model synchronization and delay phenomena in timed discrete-event systems. We specifically focus on backward reachability analysis, i.e., determining the set of states that can reach a given target set within a certain number of steps. Computing backward reachable sets presents significant challenges due to the non-convexity of max-plus dynamics and the complexity of set complement operations. To address these challenges, we propose a novel approximation framework that efficiently computes backward reachable sets by exploiting the structure of tropical polyhedra. Our approach reformulates the problem as a sequence of symbolic operations and approximates non-convex target sets through closure operations on unions of tropical polyhedra. We develop a systematic algorithm that constructs both outer (M-form) and inner (V-form) representations of the resulting sets, incorporating extremal filtering to reduce computational complexity. The proposed method offers a scalable alternative to traditional DBM-based approaches, enabling reliable approximate backward reachability analysis for general target regions in MPLS.

preprint2026arXiv

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

Signal Temporal Logic (STL) is an expressive formal language for specifying spatio-temporal requirements over real-valued, real-time signals. It has been widely used for the verification and synthesis of autonomous systems and cyber-physical systems. In practice, however, users often express their requirements in natural language rather than in structured STL formulas, making natural-language-to-STL translation a critical yet challenging task. Manual specification requires temporal-logic expertise and cannot scale, while prompting commercial LLM APIs incurs substantial token costs and may expose sensitive system requirements to third-party services, raising privacy concerns for industrial deployment. To address these challenges, we present \textsc{ReasonSTL}, a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation. \textsc{ReasonSTL} decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction. We further introduce process-rewarded training to supervise both tool-use trajectories and final formulas, together with \textsc{STL-Bench}, a bilingual, computation-aware benchmark grounded in real-world signals. Experiments show that a 4B model trained with \textsc{ReasonSTL} achieves state-of-the-art performance in both automatic metrics and human evaluations, demonstrating that \textsc{ReasonSTL} provides a transparent, low-cost, and privacy-preserving alternative for formal specification drafting.

preprint2026arXiv

Stability Verification for Switched Systems using Neural Multiple Lyapunov Functions

Stability analysis of switched systems, characterized by multiple operational modes and switching signals, is challenging due to their nonlinear dynamics. While frameworks such as multiple Lyapunov functions (MLF) provide a foundation for analysis, their computational applicability is limited for systems without favorable structure. This paper investigates stability analysis for switched systems under state-dependent switching conditions. We propose neural multiple Lyapunov functions (NMLF), a unified framework that combines the theoretical guarantees of MLF with the computational efficiency of neural Lyapunov functions (NLF). Our approach leverages a set of tailored loss functions and a counter-example guided inductive synthesis (CEGIS) scheme to train neural networks that rigorously satisfy MLF conditions. Through comprehensive simulations and theoretical analysis, we demonstrate NMLF&#39;s effectiveness and its potential for practical deployment in complex switched systems.

preprint2026arXiv

Zero-Shot Signal Temporal Logic Planning with Disjunctive Branch Selection in Dynamic Semantic Maps

Signal Temporal Logic (STL) offers verifiable task specifications and is crucial for safety-critical control. Yet STL planning remains challenging: exact optimization-based methods are often too slow, and learning-based methods struggle to generalize across varying environments. We propose a zero-shot STL planning solver for variable-map environments that generates feasible trajectories without retraining. By integrating a map-conditioned Transformer architecture with a lightweight heuristic, our approach effectively handles complex disjunctive (OR) subformulas. Furthermore, we leverage Transitive Reinforcement Learning (TRL) to ensure consistent temporal grounding and logical coherence across decomposed sub-tasks. Experiments on dynamic semantic maps with diverse obstacle layouts demonstrate consistent gains, highlighting the framework's superior zero-shot generalization to changing environments and broad STL coverage.

preprint2022arXiv

A Framework for Current-State Opacity under Dynamic Information Release Mechanism

Opacity is an important information-flow security property that characterizes the plausible deniability of a dynamic system for its &#34;secret&#34; against eavesdropping attacks. As an information-flow property, the underlying observation model is the key in the modeling and analysis of opacity. In this paper, we investigate the verification of current-state opacity for discrete-event systems under Orwellian-type observations, i.e., the system is allowed to re-interpret the observation of an event based on its future suffix. First, we propose a new Orwellian-type observation model called the dynamic information release mechanism (DIRM). In the DIRM, when to release previous &#34;hold on&#34; events is state-dependent. Then we propose a new definition of opacity based on the notion of history-equivalence rather than the standard projection-equivalence. This definition is more suitable for observations that are not prefix-closed. Finally, we show that by constructing a new structure called the DIRM-observer, current-state opacity can be effectively verified under the DIRM. Computational complexity analysis as well as illustrative examples for the proposed approach are also provided. Compared with the existing Orwellian-type observation model, the proposed framework is more general in the sense that the information-release-mechanism is state-dependent and the corresponding definition of opacity is more suitable for non-prefix-closed observations.

preprint2022arXiv

A Uniform Framework for Diagnosis of Discrete-Event Systems with Unreliable Sensors using Linear Temporal Logic

In this paper, we investigate the diagnosability verification problem of partially-observed discrete-event systems (DES) subject to unreliable sensors. In this setting, upon the occurrence of each event, the sensor reading may be non-deterministic due to measurement noises or possible sensor failures. Existing works on this topic mainly consider specific types of unreliable sensors such as the cases of intermittent sensors failures, permanent sensor failures or their combinations. In this work, we propose a novel \emph{uniform framework} for diagnosability of DES subject to, not only sensor failures, but also a very general class of unreliable sensors. Our approach is to use linear temporal logic (LTL) with semantics on infinite traces to describe the possible behaviors of the sensors. A new notion of $φ$-diagnosability is proposed as the necessary and sufficient condition for the existence of a diagnoser when the behaviors of sensors satisfy the LTL formula $φ$. Effective approach is provided to verify this notion. We show that, our new notion of $φ$-diagnosability subsumes all existing notions of robust diagnosability of DES subject to sensor failures. Furthermore, the proposed framework is user-friendly and flexible since it supports an arbitrary user-defined unreliable sensor type based on the specific scenario of the application. As examples, we provide two new notions of diagnosability, which have never been investigated in the literature, using our uniform framework.

preprint2022arXiv

Fault Diagnosis of Discrete-Event Systems under Non-Deterministic Observations with Output Fairness

In this paper, we revisit the fault diagnosis problem of discrete-event systems (DES) under non-deterministic observations. Non-deterministic observation is a general observation model that includes the case of intermittent loss of observations. In this setting, upon the occurrence of an event, the sensor reading may be non-deterministic such that a set of output symbols are all possible. Existing works on fault diagnosis under non-deterministic observations require to consider all possible observation realizations. However, this approach includes the case where some possible outputs are permanently disabled. In this work, we introduce the concept of output fairness by requiring that, for any output symbols, if it has infinite chances to be generated, then it will indeed be generated infinite number of times. We use an assume-guarantee type of linear temporal logic formulas to formally describe this assumption. A new notion called output-fair diagnosability (OF-diagnosability) is proposed. An effective approach is provided for the verification of OF-diagnosability. We show that the proposed notion of OF-diagnosability is weaker than the standard definition of diagnosability under non-deterministic observations, and it better captures the physical scenario of observation non-determinism or intermittent loss of observations.

preprint2022arXiv

Online Monitoring of Dynamic Systems for Signal Temporal Logic Specifications with Model Information

Online monitoring aims to evaluate or to predict, at runtime, whether or not the behaviors of a system satisfy some desired specification. It plays a key role in safety-critical cyber-physical systems. In this work, we propose a new model-based approach for online monitoring for specifications described by Signal Temporal Logic (STL) formulae. Specifically, we assume that the observed state traces are generated by an underlying dynamic system whose model is known. The main idea is to consider the dynamic of the system when evaluating the satisfaction of the STL formulae. To this end, effective approaches for the computation of feasible sets for STL formulae are provided. We show that, by explicitly utilizing the model information of the dynamic system, the proposed online monitoring algorithm can falsify or certify of the specification in advance compared with existing algorithms, where no model information is used. We also demonstrate the proposed monitoring algorithm by case studies.

preprint2022arXiv

Secure-by-Construction Synthesis of Cyber-Physical Systems

Correct-by-construction synthesis is a cornerstone of the confluence of formal methods and control theory towards designing safety-critical systems. Instead of following the time-tested, albeit laborious (re)design-verify-validate loop, correct-by-construction methodology advocates the use of continual refinements of formal requirements -- connected by chains of formal proofs -- to build a system that assures the correctness by design. A remarkable progress has been made in scaling the scope of applicability of correct-by-construction synthesis -- with a focus on cyber-physical systems that tie discrete-event control with continuous environment -- to enlarge control systems by combining symbolic approaches with principled state-space reduction techniques. Unfortunately, in the security-critical control systems, the security properties are verified ex post facto the design process in a way that undermines the correct-by-construction paradigm. We posit that, to truly realize the dream of correct-by-construction synthesis for security-critical systems, security considerations must take center-stage with the safety considerations. Moreover, catalyzed by the recent progress on the opacity sub-classes of security properties and the notion of hyperproperties capable of combining security with safety properties, we believe that the time is ripe for the research community to holistically target the challenge of secure-by-construction synthesis. This paper details our vision by highlighting the recent progress and open challenges that may serve as bricks for providing a solid foundation for secure-by-construction synthesis of cyber-physical systems.

preprint2022arXiv

Sensor Deception Attacks Against Initial-State Privacy in Supervisory Control Systems

This paper investigates the problem of synthesizing sensor deception attackers against privacy in the context of supervisory control of discrete-event systems (DES). We consider a DES plant controlled by a supervisor, which is subject to sensor deception attacks. Specifically, we consider an active attacker that can tamper with the observations received by the supervisor by, e.g., hacking on the communication channel between the sensors and the supervisor. The privacy requirement of the supervisory control system is to maintain initial-state opacity, i.e., it does not want to reveal the fact that it was initiated from a secret state during its operation. On the other hand, the attacker aims to deceive the supervisor, by tampering with its observations, such that initial-state opacity is violated due to incorrect control actions. In this work, we investigate from the attacker&#39;s point of view by presenting an effective approach for synthesizing sensor attack strategies threatening the privacy of the system. To this end, we propose the All Attack Structure (AAS) that records state estimates for both the supervisor and the attacker. This structure serves as a basis for synthesizing a sensor attack strategy. We also discuss how to simplify the synthesis complexity by leveraging the structural property of the initial-state privacy requirement. A running academic example is provided to illustrate the synthesis procedure.

preprint2022arXiv

Towards a Theory of Faithfulness: Faithful Explanations of Differentiable Classifiers over Continuous Data

There is broad agreement in the literature that explanation methods should be faithful to the model that they explain, but faithfulness remains a rather vague term. We revisit faithfulness in the context of continuous data and propose two formal definitions of faithfulness for feature attribution methods. Qualitative faithfulness demands that scores reflect the true qualitative effect (positive vs. negative) of the feature on the model and quanitative faithfulness that the magnitude of scores reflect the true quantitative effect. We discuss under which conditions these requirements can be satisfied to which extent (local vs global). As an application of the conceptual idea, we look at differentiable classifiers over continuous data and characterize Gradient-scores as follows: every qualitatively faithful feature attribution method is qualitatively equivalent to Gradient-scores. Furthermore, if an attribution method is quantitatively faithful in the sense that changes of the output of the classifier are proportional to the scores of features, then it is either equivalent to gradient-scoring or it is based on an inferior approximation of the classifier. To illustrate the practical relevance of the theory, we experimentally demonstrate that popular attribution methods can fail to give faithful explanations in the setting where the data is continuous and the classifier differentiable.

preprint2022arXiv

Towards Realistic Visual Dubbing with Heterogeneous Sources

The task of few-shot visual dubbing focuses on synchronizing the lip movements with arbitrary speech input for any talking head video. Albeit moderate improvements in current approaches, they commonly require high-quality homologous data sources of videos and audios, thus causing the failure to leverage heterogeneous data sufficiently. In practice, it may be intractable to collect the perfect homologous data in some cases, for example, audio-corrupted or picture-blurry videos. To explore this kind of data and support high-fidelity few-shot visual dubbing, in this paper, we novelly propose a simple yet efficient two-stage framework with a higher flexibility of mining heterogeneous data. Specifically, our two-stage paradigm employs facial landmarks as intermediate prior of latent representations and disentangles the lip movements prediction from the core task of realistic talking head generation. By this means, our method makes it possible to independently utilize the training corpus for two-stage sub-networks using more available heterogeneous data easily acquired. Besides, thanks to the disentanglement, our framework allows a further fine-tuning for a given talking head, thereby leading to better speaker-identity preserving in the final synthesized results. Moreover, the proposed method can also transfer appearance features from others to the target speaker. Extensive experimental results demonstrate the superiority of our proposed method in generating highly realistic videos synchronized with the speech over the state-of-the-art.

preprint2022arXiv

You Don&#39;t Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems

In this paper, we investigate a class of information-flow security properties called opacity in partial-observed discrete-event systems. Roughly speaking, a system is said to be opaque if the intruder, which is modeled by a passive observer, can never determine the &#34;secret&#34; of the system for sure. Most of the existing notions of opacity consider secrets related to the actual behaviors of the system. In this paper, we consider a new type of secret related to the knowledge of the system user. Specifically, we assume that the system user also only has partial observation of the system and has to reason the actual behavior of the system. We say a system is high-order opaque if the intruder can never determine that the system user knows some information of importance based on its own incomparable information. We provide the formal definition of high-order opacity. Two algorithms are provided for the verification of this new notion: one with doubly-exponential complexity for the worst case and the other with single-exponential complexity. Illustrative examples are provided for the new notion of high-order opacity.

preprint2021arXiv

ByteSing: A Chinese Singing Voice Synthesis System Using Duration Allocated Encoder-Decoder Acoustic Models and WaveRNN Vocoders

This paper presents ByteSing, a Chinese singing voice synthesis (SVS) system based on duration allocated Tacotron-like acoustic models and WaveRNN neural vocoders. Different from the conventional SVS models, the proposed ByteSing employs Tacotron-like encoder-decoder structures as the acoustic models, in which the CBHG models and recurrent neural networks (RNNs) are explored as encoders and decoders respectively. Meanwhile an auxiliary phoneme duration prediction model is utilized to expand the input sequence, which can enhance the model controllable capacity, model stability and tempo prediction accuracy. WaveRNN neural vocoders are also adopted as neural vocoders to further improve the voice quality of synthesized songs. Both objective and subjective experimental results prove that the SVS method proposed in this paper can produce quite natural, expressive and high-fidelity songs by improving the pitch and spectrogram prediction accuracy and the models using attention mechanism can achieve best performance.

preprint2021arXiv

End-to-End Learning for Simultaneously Generating Decision Map and Multi-Focus Image Fusion Result

The general aim of multi-focus image fusion is to gather focused regions of different images to generate a unique all-in-focus fused image. Deep learning based methods become the mainstream of image fusion by virtue of its powerful feature representation ability. However, most of the existing deep learning structures failed to balance fusion quality and end-to-end implementation convenience. End-to-end decoder design often leads to unrealistic result because of its non-linear mapping mechanism. On the other hand, generating an intermediate decision map achieves better quality for the fused image, but relies on the rectification with empirical post-processing parameter choices. In this work, to handle the requirements of both output image quality and comprehensive simplicity of structure implementation, we propose a cascade network to simultaneously generate decision map and fused result with an end-to-end training procedure. It avoids the dependence on empirical post-processing methods in the inference stage. To improve the fusion quality, we introduce a gradient aware loss function to preserve gradient information in output fused image. In addition, we design a decision calibration strategy to decrease the time consumption in the application of multiple images fusion. Extensive experiments are conducted to compare with 19 different state-of-the-art multi-focus image fusion structures with 6 assessment metrics. The results prove that our designed structure can generally ameliorate the output fused image quality, while implementation efficiency increases over 30\% for multiple images fusion.

preprint2021arXiv

Optimal Synthesis of Opacity-Enforcing Supervisors for Qualitative and Quantitative Specifications

In this paper, we investigate both qualitative and quantitative synthesis of optimal privacy-enforcing supervisors for partially-observed discrete-event systems. We consider a dynamic system whose information-flow is partially available to an intruder, which is modeled as a passive observer. We assume that the system has a &#34;secret&#34; that does not want to be revealed to the intruder. Our goal is to synthesize a supervisor that controls the system in a least-restrictive manner such that the closed-loop system meets the privacy requirement. For the qualitative case, we adopt the notion of infinite-step opacity as the privacy specification by requiring that the intruder can never determine for sure that the system is/was at a secret state for any specific instant. If the qualitative synthesis problem is not solvable or the synthesized solution is too restrictive, then we further investigate the quantitative synthesis problem so that the secret is revealed (if unavoidable) as late as possible. Effective algorithms are provided to solve both the qualitative and quantitative synthesis problems. Specifically, by building suitable information structures that involve information delays, we show that the optimal qualitative synthesis problem can be solved as a safety-game. The optimal quantitative synthesis problem can also be solved as an optimal total-cost control problem over an augmented information structure. Our work provides a complete solution to the standard infinite-step opacity control problem, which has not been solved without assumption on the relationship between controllable events and observable events. Furthermore, we generalize the opacity enforcement problem to the numerical setting by introducing the secret-revelation-time as a new quantitative measure.

preprint2020arXiv

A hybrid text normalization system using multi-head self-attention for mandarin

In this paper, we propose a hybrid text normalization system using multi-head self-attention. The system combines the advantages of a rule-based model and a neural model for text preprocessing tasks. Previous studies in Mandarin text normalization usually use a set of hand-written rules, which are hard to improve on general cases. The idea of our proposed system is motivated by the neural models from recent studies and has a better performance on our internal news corpus. This paper also includes different attempts to deal with imbalanced pattern distribution of the dataset. Overall, the performance of the system is improved by over 1.5% on sentence-level and it has a potential to improve further.

preprint2020arXiv

Improving Accent Conversion with Reference Encoder and End-To-End Text-To-Speech

Accent conversion (AC) transforms a non-native speaker&#39;s accent into a native accent while maintaining the speaker&#39;s voice timbre. In this paper, we propose approaches to improving accent conversion applicability, as well as quality. First of all, we assume no reference speech is available at the conversion stage, and hence we employ an end-to-end text-to-speech system that is trained on native speech to generate native reference speech. To improve the quality and accent of the converted speech, we introduce reference encoders which make us capable of utilizing multi-source information. This is motivated by acoustic features extracted from native reference and linguistic information, which are complementary to conventional phonetic posteriorgrams (PPGs), so they can be concatenated as features to improve a baseline system based only on PPGs. Moreover, we optimize model architecture using GMM-based attention instead of windowed attention to elevate synthesized performance. Experimental results indicate when the proposed techniques are applied the integrated system significantly raises the scores of acoustic quality (30$\%$ relative increase in mean opinion score) and native accent (68$\%$ relative preference) while retaining the voice identity of the non-native speaker.

preprint2020arXiv

Modeling and Analysis of Networked Discrete Event Systems with Multiple Control Channels

In this paper, we propose a novel framework for modeling and analysis of networked discrete-event systems (DES). We assume that the plant is controlled by a feedback supervisor whose control decisions are subject to communication delays and losses. Furthermore, we consider a general setting where the supervisor sends control decisions to different actuators via different communication channels whose dynamics are independent. We provide a system theoretic approach by identifying the state-space of overall networked system and investigating the dynamic of the entire state-space. Our approach precisely specifies the roles of the supervisor, the communication channels and the actuators. Also, we compare the proposed networked DES model with the existing one and show that the proposed networked model captures physical situations of networked systems more precisely.

preprint2020arXiv

Xiaomingbot: A Multilingual Robot News Reporter

This paper proposes the building of Xiaomingbot, an intelligent, multilingual and multimodal software robot equipped with four integral capabilities: news generation, news translation, news reading and avatar animation. Its system summarizes Chinese news that it automatically generates from data tables. Next, it translates the summary or the full article into multiple languages, and reads the multilingual rendition through synthesized speech. Notably, Xiaomingbot utilizes a voice cloning technology to synthesize the speech trained from a real person&#39;s voice data in one input language. The proposed system enjoys several merits: it has an animated avatar, and is able to generate and read multilingual news. Since it was put into practice, Xiaomingbot has written over 600,000 articles, and gained over 150,000 followers on social media platforms.