Solvability of Approximate Reach-Avoid Games
Mario Gleirscher
TL;DR
The paper addresses online synthesis of robust reach-avoid controllers for parametric, disturbed nonlinear systems by modeling the problem as a parametric weighted hybrid game automaton and solving online with scope-adaptive discrete dynamic programming. It proves a solvability theorem using a numerical Hamilton-Jacobi-Isaacs equation as an inductive invariant for the incrementally computed winning region and identifies the necessary and sufficient conditions for solvability. Under these conditions, it derives a decision procedure for approximate modal reach-avoid games with a $\\mathcal{O}(N|\\mathbb{X}||\\mathcal{U}||\\mathcal{D}|)$-time algorithm, enabling $\,\\delta$-robust bounded correctness and $N$-stage liveness. This work thus provides a concrete, online, and scalable approach to safe-and-close-to-optimal control in cyber-physical systems with potential certification relevance and guides future integration with assurance workflows and advanced RL variants.
Abstract
Objective: In a companion paper, we propose a parametric hybrid automaton model and an algorithm for the online synthesis of robustly correct and near-optimal controllers for cyber-physical system with reach-avoid guarantees. A key part of this synthesis problem is based on a weighted discretised game and solved via scope-adaptive discrete dynamic programming. Approach: This work examines proofs of key properties of the discussed algorithm. Evaluation: The main proof is by induction over the stages of a discrete Hamilton-Jacobi-Bellman system of equations. Contribution: The results include a game solvability theorem and identify necessary and sufficient conditions for its applicability.