Uniform Substitution At One Fell Swoop

TL;DR

This paper introduces a linear, one-pass uniform substitution mechanism for differential game logic, ensuring soundness and completeness in hybrid systems and hybrid games by using a variable condition.

Contribution

It presents a novel one-pass uniform substitution method that simplifies and ensures soundness in differential game logic for hybrid systems and games.

Findings

Proves soundness of the substitution method

Establishes completeness of the approach

Demonstrates applicability to hybrid systems and games

Abstract

Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks, this paper introduces a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacements performed by the substitution. The setting in this paper is that of differential hybrid games, in which discrete, continuous, and adversarial dynamics interact in differential game logic dGL. This paper proves soundness and completeness of one-pass uniform substitutions for dGL.