Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this paper, we investigate the verification of diagnosability for cyber-physical systems with continuous state sets. We develop an abstraction-free and automata-based framework to verify (the lack of) diagnosability, leveraging a notion of hybrid barrier certificates. To this end, we first construct a ($\delta,K$)-deterministic finite automaton that captures the occurrence of faults targeted for diagnosis. Then, the verification of diagnosability property is converted into a safety verification problem over a product system between the automaton and the augmented version of the dynamical system. We demonstrate that this verification problem can be addressed by computing hybrid barrier certificates for the product system. To this end, we introduce two systematic methods, leveraging sum-of-squares programming and counter-example guided inductive synthesis to search for such certificates. Additionally, if the system is found to be diagnosable, we propose methodologies to construct a diagnoser to identify fault occurrences online. Finally, we showcase the effectiveness of our methods through a case study.

Data-driven approaches with formal guarantees have recently emerged as a powerful means for the verification and controller synthesis of complex dynamical systems. Interest in these methods is rapidly growing, as system models are often unavailable in practice, and challenges such as nonlinear behavior, uncertainty, and the curse of dimensionality typically render accurate modeling infeasible. These difficulties motivate leveraging limited data collected from the system while still providing formal guarantees on its overall behavior. The community has therefore proposed a few hundred articles on the development of data-driven frameworks that enable the formal verification and synthesis of dynamical systems without explicit models, addressing complex specifications beyond stability. Despite this rapid growth, existing results remain scattered and lack a coherent organization, limiting a clear understanding of their principles, distinctions, and practical potential. This survey fills this gap by providing a comprehensive overview of these data-driven methods for both deterministic and stochastic dynamical systems. We structure the literature around three main methodological pillars in formal methods: (in)finite-abstraction-based techniques, functional certificate approaches, such as control barrier certificates, and compositional methods. For each of these approaches, we classify the resulting data-driven guarantees into three main categories: (i) statistical guarantees grounded in probably approximately correct and scenario-based frameworks, (ii) guarantees derived from Lipschitz continuity, and (iii) guarantees exploiting structural properties. While the literature on deterministic systems is considerably richer, we also devote particular attention to the stochastic counterpart, highlighting the inherent differences and challenges that arise compared to the deterministic case.

A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute omega-regular specifications by separating consecutive transitions of omega-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We provide SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness via a paradigmatic case study.

This paper introduces a general approximate alternating simulation relation (ε-gAAS relation) for continuous-time systems, which relaxes existing simulation relations to tolerate larger mismatches between abstract and concrete models. The definition of gAAS for continuous-time systems is first proposed, and its properties are investigated. Then, a control refinement method is developed to enable hierarchical control for the gAAS relation. Finally, case studies demonstrate the effectiveness of the proposed approach, highlighting its advantages over existing methods.

Regression models are vulnerable to adversarial corruptions during both training and testing, yet existing robustness certificates are often classification-oriented or restricted to specific models, attacks, or budget parametrizations. We develop a unified control-theoretic framework for certifying robustness of regression models by modeling training as a discrete-time dynamical system (dt-DS) and formulating terminal performance degradation as a safety property. The resulting terminal-time verification problem is addressed using time-dependent barrier certificates (TDBCs). To avoid analytical certificate construction for modern learning pipelines, we learn a neural network-based barrier certificate (NNBC) from sampled trajectories and validate it via a scenario convex problem (SCP), yielding a Probably Approximately Correct (PAC) guarantee. Experiments on diverse regression tasks demonstrate non-trivial certified attack budgets while remaining agnostic to the model, loss, attack type, and budget parametrization.

This paper presents a novel data-driven framework for the robust safety verification and safe control synthesis of unknown monotone discrete-time systems. While existing data-driven safety analysis approaches are often either heuristic in nature or require large amounts of data to provide rigorous guarantees, we leverage the structural property of monotonicity to significantly reduce data requirements while still ensuring formal safety guarantees. Our approach is built upon a new class of certificates called dominance functions, constructed directly from collected system trajectories, which themselves need not be safe. By exploiting the monotone structure of the dynamics, we show that dominance functions are (i) dissipative, meaning that they decrease monotonically along system trajectories, and (ii) sufficiently to characterize safety certificates for monotone systems. Together, these properties establish dominance functions as principled building blocks for the systematic construction of formal safety certificates directly from trajectory data. For both robust safety verification and safe control synthesis, we develop an efficient sampling-based optimization framework that searches for safety certificates represented as linear combinations of dominance functions constructed from collected trajectories. We validate our data-driven framework on two monotone systems by successfully deriving safety certificates from a small number of trajectories.

We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of HyperCertificates. Unlike linear temporal logic (LTL) formulae which are concerned with individual traces of a system, hyperproperties are properties that are concerned with how the traces of a system relate to one another. HyperLTL is an extension of LTL for hyperproperties, and is useful to describe specifications such as opacity, privacy as well as notions of robustness. Our notion of HyperCertificates consists of a pair of functions, where the first models the lookahead, and the second relies on a combination of barrier and ranking functions. We use closure certificates, to act as a model for this lookahead and then rely on barrier and ranking function arguments modulo this lookahead to provide guarantees against HyperLTL formulae. We demonstrate how our approach is automatable via existing techniques such as sum-of-squares optimization (SOS) and satisfiability modulo theories (SMT) solvers. Finally, we demonstrate our approach on some case studies.

The recently introduced notions of ranking functions and closure certificates utilize well-foundedness arguments to facilitate the verification of dynamical systems against ω-regular properties. A ranking function and a closure certificate are real-valued functions defined over states and state pairs of a dynamical system whose zero superlevel sets are inductive state invariant and inductive transition invariant, respectively. The search for such certificates can be automated by fixing a specific template class, such as a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, such certificates may not be found for a fixed template. In such a case, one must change the template; for example, increase the degree of the polynomial. In this paper, we consider a notion of multiple functions in the form of vector certificates. Taking inspiration from the literature on vector barrier certificates as generalizations of standard barrier certificates for safety verification, we propose vector co-Büchi ranking functions and vector closure certificates as nontrivial generalizations of ranking functions and closure certificates, respectively. Both notions consist of a set of functions that jointly overapproximate an inductive invariant by considering each function to be a linear combination of the others. The advantage of such certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present an SOS programming approach to search for these functions and demonstrate the effectiveness of our proposed method in verifying ω-regular specifications in several case studies.

The increasing use of machine learning in safety-critical domains amplifies the risk of adversarial threats, especially data poisoning attacks that corrupt training data to degrade performance or induce unsafe behavior. Most existing defenses lack formal guarantees or rely on restrictive assumptions about the model class, attack type, extent of poisoning, or point-wise certification, limiting their practical reliability. This paper introduces a principled formal robustness certification framework that models gradient-based training as a discrete-time dynamical system (dt-DS) and formulates poisoning robustness as a formal safety verification problem. By adapting the concept of barrier certificates (BCs) from control theory, we introduce sufficient conditions to certify a robust radius ensuring that the terminal model remains safe under worst-case ${\ell }_{p}$-norm based poisoning. To make this practical, we parameterize BCs as neural networks trained on finite sets of poisoned trajectories. We further derive probably approximately correct (PAC) bounds by solving a scenario convex program (SCP), which yields a confidence lower bound on the certified robustness radius generalizing beyond the training set. Importantly, our framework also extends to certification against test-time attacks, making it the first unified framework to provide formal guarantees in both training and test-time attack settings. Experiments on MNIST, SVHN, CIFAR-10, and CIFAR-100 show that our approach certifies non-trivial perturbation budgets while being model-agnostic and requiring no prior knowledge of the attack or contamination level.

In traditional hierarchical control strategies, controllers are typically constructed by refining the controllers developed for an abstract system to a concrete system through a simulation relation established over the state sets of both systems. Nonetheless, this approach can lead to significant discrepancies between the abstract and concrete systems, thereby limiting the effectiveness of hierarchical control. To overcome this challenge, we present a more adaptable simulation relation called the general approximate alternating simulation relation, which also incorporates the input set of the abstract system. This new simulation relation reflects the similarities between the abstract and concrete systems more accurately, subsuming conventional alternating simulation relations. Moreover, it refines the hierarchical control structure by further reducing the discrepancy in outputs between the actual system and its abstract model. We propose methodologies for applying this relation in two scenarios: (1) discrete-time control systems with finite state and input sets, and (2) linear control systems and their continuous-space abstractions.

Resilience in cyber-physical systems (CPS) is the fundamental ability to maintain safety and critical functionality despite adverse "perturbations," which includes security attacks, environmental disruptions, and hardware or software failures. This survey provides a comprehensive review of CPS resilience, framing the field through five interconnected themes that are required in an integrated whole to achieve real-world resilience. The article first posits that resilience is a system-wide property emerging from interactions between hardware, software, and human users. Second, it addresses the challenges of learning-enabled CPS, which often operate in data-scarce environments characterized by imbalanced or noisy data, requiring innovative solutions like synthetic data generation and foundation model adaptation. Third, the survey examines proactive measures for resilience, which include distinctive aspects of verification, testing, and redundancy. Fourth, it explores recovery mechanisms, moving beyond traditional fault models to design "just good enough" recovery strategies that prioritize safety-critical functions during perturbations. Finally, it highlights the central role of the human, focusing on the different levels of human intervention, the necessity of trust calibration, and the requirement for explainable AI to support human-CPS teaming. These themes are illustrated through representative application domains, primarily Connected and Autonomous Transportation Systems (CATS) and Medical CPS (MCPS). By integrating the five interconnected themes, this survey provides a systematic roadmap for achieving the resilient CPS in increasingly complex and adversarial environments.

In this paper, we present the synthesis of secure-by-construction controllers that address safety and security properties simultaneously in cyber-physical systems. Our focus is on studying a specific security property called opacity, which characterizes the system's ability to maintain plausible deniability of its secret behavior in the presence of an intruder. These controllers are synthesized based on a concept of so-called (augmented) control barrier functions, which we introduce and discuss in detail. We propose conditions that facilitate the construction of the desired (augmented) control barrier functions and their corresponding secure-by-construction controllers. To compute these functions, we propose an iterative scheme that leverages iterative sum-of-square programming techniques. This approach enables efficient computation of these functions, particularly for polynomial systems. Moreover, we demonstrate the flexibility of our approach by incorporating user-defined cost functions into the construction of secure-by-construction controllers. Finally, we validate the effectiveness of our results through two case studies, illustrating the practical applicability and benefits of our proposed approach.

This paper introduces a notion of backward control barrier certificates to synthesize safety controllers for deterministic systems. Barrier certificates and control barrier certificates play a fundamental role in the automated design of controllers to ensure the safety of dynamical systems. The simultaneous search for control barrier certificates and their controllers typically face challenges in automation as they involve quantifier alternation between the states (for all states) and the inputs (there exists an input) as well as bilinearity between the unknown certificate and control input. In this paper, we show that one may simultaneously search for both a certificate and controller effectively for deterministic systems via standard sum-of-squares approaches without the need for quantifier alternation. Here, we treat the input as a disturbance and build an invariant set over the unsafe set of states rather the the initial set. This set is invariant in the backward direction rather than forward, and hence we dub these as backward control barrier certificates. Ensuring that the initial set is not in this invariant set guarantees the existence of a controller to ensure safety. We show how one may automate the search for these certificates, and discuss some strategies to implement their corresponding safety controllers. Finally, we demonstrate the efficacy of our approach with some case studies.

This paper explores a neurosymbolic approach to probabilistic transfer of control logic from a source stochastic control system to a target system while ensuring approximately equivalent behavioral guarantees in both domains. Traditional methods struggle with this problem due to the absence of a complete characterization of behavioral specifications, which prevents a direct formulation in terms of loss functions. To address this challenge, we leverage the concept of stochastic simulation relations to establish probabilistic observational equivalence between the behaviors of two (blackbox) stochastic systems. These functions ensure that the outputs of both systems, equipped with their respective controllers, remain probabilistically close over time. By parameterizing stochastic simulation functions with neural networks, we introduce the notion of stochastic neural simulation functions, enabling a data-driven mechanism to transfer any synthesized controller-along with its proof of correctness-without requiring explicit specification of behavioral constraints. This neurosymbolic integration combines the scalability of neural methods with the formal guarantees of symbolic approaches, bridging the gap between learning-based control synthesis and formal verification. Compared to prior methods, our approach eliminates the need for a closed-loop mathematical model and explicit requirement specifications for both the source and target systems, while providing probabilistic guarantees over an infinite horizon. We also introduce validity conditions that, when satisfied, ensure the closeness of the outputs of two systems equipped with their corresponding controllers, removing the need for post-facto verification. We demonstrate the effectiveness of our approach through four case studies, highlighting its potential to advance scalable, formally grounded, and transferable control synthesis.

Reward machines (RMs) provide a structured way to specify non-Markovian rewards in reinforcement learning (RL), thereby improving both expressiveness and programmability. Viewed more broadly, they separate what is known about the environment, captured by the reward mechanism, from what remains unknown and must be discovered through sampling. This separation supports techniques such as counterfactual experience generation and reward shaping, which reduce sample complexity and speed up learning. We introduce physics-informed reward machines (pRMs), a symbolic machine designed to express complex learning objectives and reward structures for RL agents, thereby enabling more programmable, expressive, and efficient learning. We present RL algorithms capable of exploiting pRMs via counterfactual experiences and reward shaping. Our experimental results show that these techniques accelerate reward acquisition during the training phases of RL. We demonstrate the expressiveness and effectiveness of pRMs through experiments in both finite and continuous physical environments, illustrating that incorporating pRMs significantly improves learning efficiency across several control tasks.

Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, modeling errors, or environmental disturbances. Traditional model-based approaches rely on precise system dynamics, which may not be available in real-world scenarios. To address this, we propose a data-driven safety verification framework that leverages matrix zonotopes and barrier certificates to verify system safety directly from noisy data. Instead of trusting a single unreliable model, we construct a set of models that capture all possible system dynamics that align with the observed data, ensuring that the true system model is always contained within this set. This model set is compactly represented using matrix zonotopes, enabling efficient computation and propagation of uncertainty. By integrating this representation into a barrier certificate framework, we establish rigorous safety guarantees without requiring an explicit system model. Numerical experiments demonstrate the effectiveness of our approach in verifying safety for dynamical systems with unknown models, showcasing its potential for real-world CPS applications.

The design of controllers with correctness guarantees is a primary concern for safety-critical control systems. A Control Barrier Certificate (CBC) is a real-valued function over the state space of the system that provides an inductive proof of the existence of a safe controller. Recently, neural networks have been successfully deployed for data-driven learning of control barrier certificates. These approaches encode the conditions for the existence of a CBC using a rectified linear unit ( ) loss function. The resulting encoding, while sound, tends to be conservative, which results in slower training and limits scalability to large, complex systems. Can altering the loss function alleviate some of the problems associated with loss and lead to faster learning? This paper proposes a novel encoding with a Mean Squared Error loss function, which allows for more scalable and efficient training, while addressing some of the theoretical limitations of previous methods. We also encode one of the main conditions of CBC in a non-conservative way, enabling us to derive CBC where existing methods have failed. The proposed approach derives a validity condition based on Lipschitz continuity to formally characterize safety guarantees, eliminating the need for a post-hoc verification. The effectiveness of the proposed loss functions is demonstrated through six case studies curated from the existing literature. Our results provide a strong argument for exploring alternative loss function choices as a novel approach to optimizing the design of CBCs.

This paper investigates controller synthesis for discrete-time stochastic control systems with unknown dynamics and unknown noise distribution, using control barrier certificates (CBCs) to ensure safety. Due to uncertainties and the lack of precise models, traditional model-based safety verification methods are often impractical for real-world cyber-physical systems. To address these challenges, we propose a data-driven framework that represents both the CBC and the associated controller as neural networks trained on a finite set of samples. Unlike prior work, our method jointly synthesizes the CBC and the controller without relying on model knowledge or predefined functional forms, and without requiring a posteriori validation. Our approach provides a probabilistic safety guarantee by establishing a lower bound on the probability of satisfying the safety specifications with a desired confidence level. Furthermore, by introducing a Lipschitz continuity-based validity condition and integrating it into the training process, we ensure that safety requirements hold not only for the training data but across the entire state set. Finally, we validate our approach on an inverted pendulum, demonstrating formal safety guarantees under uncertainty.

We present a data-driven methodology for verifying dynamical systems against specifications defined by universal co-Buchi automata (UCA), even when only a black-box simulator of the system is available. Our approach leverages the recently introduced concept of closure certificates (CCs), which are particularly well-suited for verifying properties that require a finite number of visits to specific regions of the state space. We begin by defining a parameterized function template for the CC. Then, we formulate the search for suitable parameters as a Scenario Optimization Program (SOP), subject to the conditions constrained by the requirements for a valid CC. To solve the SOP, we collect samples from the state space, either deterministically or probabilistically, and ultimately produce a candidate CC. Under probabilistic sampling, we provide a Probably Approximately Correct (PAC) guarantee, while deterministic sampling yields a deterministic 100% guarantee. Finally, we demonstrate the effectiveness of the proposed framework using a three-tank model, highlighting the practical applicability and performance.