Abstract This paper introduces robust differential dynamic logic (a fragment of differential dynamic logic) to specify and reason about robust hybrid systems . By small, natural, and practically meaningful syntactic restrictions, specifications are ensured (by construction) to be topologically open and, thus, robust with respect to infinitesimal perturbations without explicit quantitative margins of error in the syntax or in proofs. The main result is a proof of absolute completeness of robust differential dynamic logic for reachability properties of general hybrid systems. The proof is constructive, self-contained, and demonstrates how robustly-correct hybrid systems reachability specifications can be automatically verified through proof.

Game logic with sabotage (GLs) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. GLs can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, GLs is exactly as expressive as the modal μ-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. A natural Hilbert-style proof calculus for GLs is presented and proved complete using syntactic equiexpressiveness reductions. The completeness of a simple extension of Parikh's calculus for game logic follows.