In this paper, we are concerned with the stability of 2-soliton solutions on a nonzero constant background for the modified Camassa-Holm equation with cubic nonlinearity. By employing conserved quantities in terms of the momentum variable m, we show that the 2-soliton, when regarded as a solution to the initial-value problem for the modified Camassa-Holm equation, is nonlinearly stable to perturbations with respect to the momentum variable in the Sobolev space H^2.

This article proposes a universal state-estimate-intersection (SEI)-based protocols for decentralized problems of discrete-event systems. The decentralized problems include control problems and diagnosis problems. Our SEI-protocol is termed "universal" in the sense that, for a fixed plant representation, it solves a larger class of problems than prior SEI-protocols. In fact, we formalize how our solution achieves as much as can be achieved by SEI-based architectures. Solution existence, verification, and construction are given. The results are formally verified by Isabelle/HOL.

Networked systems must often balance privacy in avoiding leaking sensitive information, with utility in communicating the information that is needed by components to operate correctly. We consider the problem of enforcing privacy and utility with both obfuscation (altering communications to mislead eavesdroppers) and control (restricting system behavior to avoid information leakage). We present a formulation of this problem that models components of the networked system as interconnected reactive processes. Tools from distributed reactive synthesis are then used to automatically design obfuscators and controllers, which coordinate to enforce requirements. In particular, we develop formal specifications capturing privacy using the information flow property of opacity and utility ensuring availability of information or imposing constraints on the closed-loop system. This synthesis approach is applicable to a large class of network architectures, which we demonstrate on three representative problems over a building access control system.

This paper presents a general framework for joint opacity of discrete-event systems under partial observation. It discusses a class of state-estimate-intersection-based (SEI-based) intrusions that existing opacity conditions cannot prevent. The paper provides a procedure to verify the opacity of a system against such SEI-based intrusions. The results are formally verified by Isabelle/HOL. (c) 2025 Elsevier Ltd. All rights are reserved, including those for text and data mining, AI training, and similar technologies.

The authors consider the property of detectability of discrete event systems in the presence of sensor attacks in the context of cyber-security. The authors model the system using an automaton and study the general notion of detectability where a given set of state pairs needs to be(eventually or periodically) distinguished in any estimate of the state of the system. The authors adopt the ALTER sensor attack model from previous work and formulate four notions of CA-detectability in the context of this attack model based on the following attributes: strong or weak; eventual or periodic. The authors present verification methods for strong CA-detectability and weak CA-detectability. The authors present definitions of strong and weak periodic CA-detectability that are based on the construction of a verifier automaton called the augmented CA-observer. The development also resulted in relaxing assumptions in prior results on D-detectability, which is a special case of CA-detectability.

We consider a diffusive Rosenzweig-MacArthur predator-prey model in the situation when the prey diffuses at the rate much smaller than that of the predator. In a certain parameter regime, the existence of fronts in the system is known: the underlying dynamical system in a singular limit is reduced to a scalar Fisher-KPP equation and the fronts supported by the full system are small perturbations of the Fisher-KPP fronts. The existence proof is based on application of the Geometric Singular Perturbation Theory with respect to two small parameters. This paper is focused on the stability of the fronts. We analyze the stability by means of energy estimates, exponential dichotomies, the Evans function calculation, and a technique that involves constructing the unstable augmented bundles. The energy estimates provide bounds on the unstable spectrum which depend on the small parameters of the system; the bounds are inversely proportional to these parameters. We further improve these estimates by showing that the eigenvalue problem is a small perturbation of some limiting (as the modulus of the eigenvalue parameter goes to infinity) system, and that the limiting system has exponential dichotomies. Persistence of the exponential dichotomies then leads to bounds uniform in the small parameters. The main novelty of this approach is related to the fact that the limit of the eigenvalue problem is not autonomous. We then use the concept of the unstable augmented bundles and by treating these as multiscale topological structures with respect to the same two small parameters consequently as in the existence proof, we show that the stability of the fronts is also governed by the scalar Fisher-KPP equation.

This paper extends the theory of diagnosability by investigating fault diagnosis in discrete event systems under sensor attacks using finite-state automata as models. It assumes that an attacker has compromised the communication channel between the system’s sensors and the diagnostic engine. While the general attack model utilized by the attacker has been previously studied in the context of supervisory control, its application to fault diagnosis remains unexplored. The attacker possesses the capability to substitute each compromised observable event with a string from an attack language. The attack model incorporates event insertion and deletion, as well as static and dynamic attacks. To formally capture the diagnostic engine’s ability to identify faults in the presence of the attacker, a novel concept called CA-diagnosability is introduced. This extends the existing notions of CA-controllability and CA-observability. A testing procedure for CA-diagnosability is developed, and its correctness is proven. Some sufficient conditions for CA-diagnosability that can be easily checked are also proposed and proved. The paper then investigates conditions under which the role of an attacker can be reverted from malicious to benevolent, that is, to help the diagnoser to diagnose faults. The paper further applies diagnosability theory to investigate conditions under which the presence of the attacker can be detected.

We present a framework for the modelling and synthesis of sensor and actuator attacks on discrete event systems. Initially, we consider systems composed of a single plant and supervisor subject to an attack that can modify the supervisor's observations and control actions. The problem of designing stealthy attacks that can always inflict damage on the system is formulated as a standard supervisory control problem. Next, we show how to apply our framework to a decentralised system. Distributed attackers, one for each subsystem, are realised as nonconflicting supervisors that must coordinate to achieve their individual goals.

In the present work we revisit the $b$-family model of peakon equations, containing as special cases the $b=2$ (Camassa-Holm) and $b=3$ (Degasperis-Procesi) integrable examples. We establish information about the point spectrum of the peakon solutions and notably find that for suitably smooth perturbations there exists point spectrum in the right half plane rendering the peakons unstable for $b<1$. We explore numerically these ideas in the realm of fixed-point iterations, spectral stability analysis and time-stepping of the model for the different parameter regimes. In particular, we identify exact, stationary (spectrally stable) lefton solutions for $b<-1$, and for $-11$. While many of the above dynamical features had been explored in earlier studies, in the present work, we supplement them, wherever possible, with spectral stability computations.

We consider feedback control systems where sensor readings and actuator commands may be compromised by an attacker intending to damage the system. We study this problem at the supervisory layer of the control system, using discrete event systems techniques. The attacker can edit the outputs from the sensors of the system before they reach the supervisory controller as well as it can edit actuator commands before they reach the system. In this context, we formulate the problem of synthesizing a supervisor that is robust against a large class of edit attacks on the sensor readings and actuator commands. Intuitively, we search for a supervisor that guarantees the safety of the system even when sensor readings and actuator commands are compromised. Given the similarities of the investigated problem to the standard supervisory control problem, our solution methodology reduces the problem of synthesizing a robust supervisor against deception attacks to a supervisory control problem. This new and intuitive solution methodology improves upon prior work on this topic.

Control systems should enforce a desired property for both expected/modeled situations as well as unexpected/unmodeled environmental situations. Existing methods focus on designing controllers to enforce the desired property only when the environment behaves as expected. However, these methods lack discussion on how the system behaves when the environment is perturbed . In this paper, we propose an approach for analyzing discrete-state control systems with respect to their tolerance against environmental perturbations. We formally define this notion of tolerance and describe a general technique to compute it, for any given regular property. We also present a more efficient method to compute tolerance with respect to invariance properties. Moreover, we show that there exists an inherent trade-off between permissiveness and tolerance that we capture via Pareto optimality conditions. We also study the problem of synthesizing Pareto optimal controllers that achieve a minimum level of tolerance and permissiveness. We demonstrate our framework on examples involving surveillance protocols and robotic motion planning.

A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions may occasionally be violated due to modeling errors or faults. Ideally, the system guarantees its critical properties even under some of these violations, i.e., the system is robust against environmental deviations. This paper proposes a notion of robustness as an explicit, first-class property of a transition system that captures how robust it is against possible deviations in the environment. We modeled deviations as a set of transitions that may be added to the original environment. Our robustness notion then describes the safety envelope of this system, i.e., it captures all sets of extra environment transitions for which the system still guarantees a desired property. We show that being able to explicitly reason about robustness enables new types of system analysis and design tasks beyond the common verification problem stated above. We demonstrate the application of our framework on case studies involving a radiation therapy interface, an electronic voting machine, a fare collection protocol, and a medical pump device.

The salient features of the new software tool MDESops are presented. MDESops is Python-based and open-source. Its focus is the analysis and control of discrete event systems (DES) modeled by finite-state automata. MDESops has core functions to manipulate deterministic and nondeterministic automata, including parallel composition and determinization. It has functions to analyze diagnosability and opacity properties. MDESops also includes functions that implement both standard and more recent algorithmic procedures from the theory of supervisory control of DES, including synthesis of supervisors for partially-observed systems, synthesis of attackers in systems with compromised sensors, and synthesis of supervisors resilient to deception attacks. It is the hope that MDESops can serve as a useful platform for algorithm development and prototyping in DES research.

Opacity is an information-flow property capturing privacy from observers that are aware of a system's dynamics. The potential for an observer with perfect recall to reason about long histories of the system poses a challenge for opacity verification. In this letter, we address this challenge by proposing a new notion of opacity over automata, called bounded memory opacity, with respect to an observer with a bounded memory. We show that verifying this weaker notion of opacity has reduced computational complexity compared to general opacity (co- NP vs. PSPACE). Furthermore, we present a corresponding verification algorithm using an encoding to the Boolean satisfiability problem (SAT). We demonstrate this approach on randomly generated automata as well as a Web server load-hiding example.

Control systems should enforce a desired property for both expected/modeled situations as well as unexpected/unmodeled environmental situations. Existing methods focus on designing maximally permissive controllers to enforce the desired property only when the environment behaves as expected. However, these methods lack discussion on how the system behaves when the environment is perturbed. We propose an approach for analyzing discrete-state systems with respect to their permissiveness and tolerance against environmental perturbations. There is an inherent trade-off between permissiveness and tolerance that we capture via Pareto optimality conditions. We investigate this trade-off by defining Pareto optimality between permissiveness and tolerance for invariance properties. We show that memoryless controllers are sufficient to describe the Pareto front. We also study the problem of synthesizing Pareto optimal controllers that achieve a minimum level of tolerance and permissiveness.

Introduction to Traveling Waves is an invitation to research focused on traveling waves for undergraduate and masters level students. Traveling waves are not typically covered in the undergraduate curriculum, and topics related to traveling waves are usually only covered in research papers, except for a few texts designed for students. This book includes techniques that are not covered in those texts. Through their experience involving undergraduate and graduate students in a research topic related to traveling waves, the authors found that the main difficulty is to provide reading materials that contain the background information sufficient to start a research project without an expectation of an extensive list of prerequisites beyond regular undergraduate coursework. This book meets that need and serves as an entry point into research topics about the existence and stability of traveling waves. Features Self-contained, step-by-step introduction to nonlinear waves written assuming minimal prerequisites, such as an undergraduate course on linear algebra and differential equations. Suitable as a textbook for a special topics course, or as supplementary reading for courses on modeling. Contains numerous examples to support the theoretical material. Supplementary MATLAB codes available via GitHub.

Networked cyber-physical systems must balance the utility of communication for monitoring and control with the risks of revealing private information. Many of these networks, such as wireless communication, are vulnerable to eavesdrop-ping by illegitimate recipients. Obfuscation can hide information from eaves-droppers by ensuring their observations are ambiguous or misleading. At the same time, coordination with recipients can enable them to interpret obfuscated data. In this way, we propose an obfuscation framework for dynamic systems that ensures privacy against eavesdroppers while maintaining utility for legitimate recipients. We consider eavesdroppers unaware of obfuscation by requiring that their observations are consistent with the original system, as well as eaves-droppers aware of the goals of obfuscation by assuming they learn of the specific obfuscation implementation used. We present a method for bounded synthesis of solutions based upon distributed reactive synthesis and the synthesis of publicly-known obfuscators.