相关论文: Exponential-Condition-Based Barrier Certificate Ge…

Machine teaching can be viewed as optimal control for learning. Given a learner's model, machine teaching aims to determine the optimal training data to steer the learner towards a target hypothesis. In this paper, we are interested in…

Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system's behaviour can ascertain some "secret" information of the system. Deciding opacity…

In this brief paper we introduce a robust-safety notion for differential inclusions, and we propose a general framework to certify such a notion in terms of barrier functions. While existing literature studied only what we designate by…

A dynamical system is strongly robustly safe provided that it remains safe in the presence of a continuous and positive perturbation, named robustness margin, added to both the argument and the image of the right-hand side (the dynamics).…

We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is…

In this work, we study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, barrier certificates have been successfully applied for ensuring…

We study stochastic systems characterized by difference inclusions. Such stochastic differential inclusions are defined by set-valued maps involving the current state and stochastic input. For such systems, we investigate the problem of…

In this letter, we detail our randomized approach to safety-critical system verification. Our method requires limited system data to make a strong verification statement. Specifically, our method first randomly samples initial conditions…

This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our…

We present a simulation-based approach for generating barrier certificate functions for safety verification of cyber-physical systems (CPS) that contain neural network-based controllers. A linear programming solver is utilized to find a…

In this work, we propose a compositional scheme based on small-gain reasoning to synthesize safety controllers for interconnected stochastic hybrid systems. In our proposed setting, we first offer an augmented scheme that characterizes each…

This paper studies provable security guarantees for cyber-physical systems (CPS) under actuator attacks. In particular, we consider CPS safety and propose a new attack detection mechanism based on zeroing control barrier function (ZCBF)…

This paper presents a novel approach for the safe control design of systems with parametric uncertainties in both drift terms and control-input matrices. The method combines control barrier functions and adaptive laws to generate a safe…

Synthesising safe controllers from visual data typically requires extensive supervised labelling of safety-critical data, which is often impractical in real-world settings. Recent advances in world models enable reliable prediction in…

Providing non-trivial certificates of safety for non-linear stochastic systems is an important open problem that limits the wider adoption of autonomous systems in safety-critical applications. One promising solution to address this problem…

This paper presents a novel approach for augmenting proof-based verification with performance-style analysis of the kind employed in state-of-the-art model checking tools for probabilistic systems. Quantitative safety properties usually…

This paper proposes a safety-critical controller for dynamic and uncertain environments, leveraging a robust environment control barrier function (ECBF) to enhance the robustness against the measurement and prediction uncertainties…

We develop a new kind of nonnegativity certificate for univariate polynomials on an interval. In many applications, nonnegative Bernstein coefficients are often used as a simple way of certifying polynomial nonnegativity. Our proposed…

The recently introduced notions of ranking functions and closure certificates utilize well-foundedness arguments to facilitate the verification of dynamical systems against $\omega$-regular properties. A ranking function and a closure…

Ensuring safe autonomous driving in the presence of occlusions poses a significant challenge in its policy design. While existing model-driven control techniques based on set invariance can handle visible risks, occlusions create latent…