Context-triggered Games for Reactive Synthesis over Stochastic Systems via Control Barrier Certificates

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.