Safety Certificates of Stochastic Cyber-Physical Systems with Wireless Communication Networks

In this work, we propose a formal framework for safety controller synthesis of stochastic control systems with both process and measurement noises while considering wireless communication networks between sensors, controllers, and actuators. The proposed scheme relies on the utilization of control barrier certificates (CBC), enabling us to offer probabilistic safety certifications for wirelessly connected stochastic systems. Despite the existing literature on designing control barrier certificates, wireless communication networks have not been taken into account to address potential packet losses and end-to-end delays, a critical consideration for safety-critical real-world applications. In our proposed scenario, the primary aim is to construct a control barrier certificate alongside a safety controller, ensuring a lower bound on the probability of satisfying the safety property within a finite time horizon. We showcase the efficacy of our approach through multiple physical case studies involving communication networks, including a permanent magnet synchronous motor, vehicle lane-keeping system, and Moore-Greitzer jet engine with nonlinear dynamics.