BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Shaoyuan Li

Shaoyuan Li contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
eess.SYSystems and ControlFormal Languages and Automata Theorymath.OC

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
12works
0followers
4topics
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

12 published item(s)

preprint2026arXiv

Convergence Filters for Efficient Economic MPC of Non-dissipative Systems

This note presents a novel and efficient Economic Model Predictive Control (EMPC) scheme specifically designed for non-dissipative systems subject to state and input constraints. To address the stability challenge of EMPC for constrained non-dissipative systems, a new concept of convergence filters is introduced. Three alternative convergence filters are designed accordingly to be incorporated into the receding horizon optimization problem of EMPC. To improve online computational efficiency, the variable horizon approach without explicit terminal state constraints is adopted. This design allows for a flexible trade-off among convergence speed, economic performance, and computational burden via simple parameter adjustment. Moreover, sufficient conditions are rigorously derived to guarantee recursive feasibility and stability. The advantages of the proposed EMPC are validated through simulations on a classical non-dissipative continuous stirred-tank reactor.

0 citations0 reviewsNo code linkedOpen access
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.

0 citations0 reviewsNo code linkedOpen access
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's effectiveness and its potential for practical deployment in complex switched systems.

0 citations0 reviewsNo code linkedOpen access
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 "secret" 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 "hold on" 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.

0 citations0 reviewsNo code linkedOpen access
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.

0 citations0 reviewsNo code linkedOpen access
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.

0 citations0 reviewsNo code linkedOpen access
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.

0 citations0 reviewsNo code linkedOpen access
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'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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Statistically Consistent Inverse Optimal Control for Linear-Quadratic Tracking with Random Time Horizon

The goal of Inverse Optimal Control (IOC) is to identify the underlying objective function based on observed optimal trajectories. It provides a powerful framework to model expert's behavior, and a data-driven way to design an objective function so that the induced optimal control is adapted to a contextual environment. In this paper, we design an IOC algorithm for linear-quadratic tracking problems with random time horizon, and prove the statistical consistency of the algorithm. More specifically, the proposed estimator is the solution to a convex optimization problem, which means that the estimator does not suffer from local minima. This enables the proven statistical consistency to actually be achieved in practice. The algorithm is also verified on simulated data as well as data from a real world experiment, both in the setting of identifying the objective function of human tracking locomotion. The statistical consistency is illustrated on the synthetic data set, and the experimental results on the real data shows that we can get a good prediction on human tracking locomotion based on estimating the objective function. It shows that the theory and the model have a good performance in real practice. Moreover, the identified model can be used as a control target in personalized rehabilitation robot controller design, since the identified objective function describes personal habit and preferences.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

You Don'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 "secret" 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.

0 citations0 reviewsNo code linkedOpen access
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 "secret" 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.

0 citations0 reviewsNo code linkedOpen access
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.

0 citations0 reviewsNo code linkedOpen access