Partially observable safety games formalize reactive synthesis problems in which a program must make safe choices despite having incomplete information about the underlying state. In such games, correctness often depends not only on the current observable state, but also on past observations. This makes strategy synthesis very challenging, particularly in symbolic settings with infinite state and action spaces.

This paper presents a new algorithm for synthesizing winning strategies for such games. A key idea is to algorithmically separate \emph{what to remember} from \emph{how to act}. To this end, our algorithm first performs generalization from bounded executions to infer a candidate \emph{symbolic memory abstraction} that a successful strategy should use. Such an abstraction consists of a set of variables, along with an interpretation of those variables in terms of the latent state. With this abstraction in place, the second phase of the algorithm then constructs a perfect information game over memory values, which can be solved via symbolic fixpoint computation to obtain both the action policy and a suitable memory-update function.

We implemented this approach in a prototype tool called \tool\ and evaluated it on {30} benchmarks drawn from UAV and descent control, robotics, and congestion control. These benchmarks involve both continuous state variables arising from system dynamics and infinite action spaces arising from real-valued control choices. Although these benchmarks are beyond the scope of existing general-purpose methods, \tool\ solves {29} of the {30} instances, either by synthesizing a winning strategy or proving unrealizability, with a median solving time of {15.6} seconds. Furthermore, on finite-action variants where comparison with prior work is possible, \tool\ solves more instances and scales better as the action space grows.