This paper offers a formal data-driven scheme for constructing control barrier certificates (CBC) and synthesizing safety controllers for discrete-time control systems. Our framework accommodates scenarios where the mathematical model is unknown, while also considering the presence of wireless communication networks between sensor-controller and controller-actuator links. While existing literature extensively addresses the design of CBC, there has been a notable lack of attention in incorporating wireless communication networks to tackle potential packet losses. This gap poses a greater challenge when considering the absence of knowledge about the system’s model, a crucial aspect in real-world applications. Given a particular rank condition for unknown wirelessly-connected systems, our method provides a linear matrix inequality, constructed based on two input-output trajectories of the system, offering a probabilistic safety assurance across an infinite time horizon. We showcase the efficacy of our data-driven approach over a wirelessly-connected synchronous motor with an unknown model.

In this paper, we offer a formal framework to automatically synthesize a hybrid controller for continuous-time nonlinear stochastic control systems while addressing control challenges closely integrated with logical decision-making processes. The primary goal is to enforce complex logic specifications that encompass context switches initiated by either the external environment or the system itself. The proposed game-solving framework adopts a two-layer strategy synthesis approach: (i) in the lower layer, it employs control barrier certificates to synthesize controllers that guarantee reach-while-avoid specifications over complex stochastic systems, and (ii) these controllers are subsequently utilized in a higher logical layer during a game-based logical control synthesis process. This approach enables the utilization of computational capabilities derived from state space control techniques and taps into the problem-solving intelligence inherent in finite games to handle complex logic specifications. We demonstrate the efficacy of our proposed approach over a robotic case study.

This work studies formal verification of continuous-time continuous-space systems with unknown dynamics against safety specifications. The proposed framework is based on a data-driven construction of barrier certificates using which the safety of unknown systems is verified via a finite set of data collected from trajectories of systems with a priori guaranteed confidence. In the proposed scheme, we first cast the original safety problem as a robust convex program (RCP). Since the unknown model appears in one of the constraints of the proposed RCP, we provide the scenario convex program (SCP) corresponding to the original RCP by collecting finite numbers of data from systems' evolutions. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP. Accordingly, we formally quantify the safety guarantee of unknown systems based on the number of data and the required level of safety confidence.

In this work, we propose a data-driven technique for a formal estimation of infinitesimal generators of continuous-time stochastic systems with unknown dynamics. In the proposed framework, we first approximate the infinitesimal generator of the solution process via a set of data collected from solution processes of unknown systems. We then put some proper assumptions on dynamics of systems and quantify the closeness between the infinitesimal generator and its approximation while providing a priori guaranteed confidence bound. We show that both the time discretization and the number of data play significant roles in providing a reasonable closeness precision.