# How to Win First-Order Safety Games

## TL;DR

This paper introduces a novel approach to synthesize strategies for first-order safety games, enabling the verification of parametric systems like network protocols and multi-agent workflows through logical and automata-theoretic techniques.

## Contribution

It generalizes FO transition systems to FO safety games, establishing a link to second-order quantifier elimination and providing classification and synthesis methods for these games.

## Key findings

- Decidable and undecidable cases for FO games with monadic predicates identified.
- Abstraction and refinement techniques enable FO strategy synthesis.
- Application demonstrated in leader election and conference management systems.

## Abstract

First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Desirable properties of these systems such as functional correctness or noninterference have conveniently been formulated as safety properties. In order to automatically synthesize strategies that enforce safety or noninterference, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is in fact, equivalent to second-order quantifier elimination. For the important case of FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of noninterference properties. Based on general techniques for second-order quantifier elimination, we provide abstraction and refinement techniques in order to synthesize FO strategies that enforce safety. We demonstrate the usefulness of our approach by inferring nontrivial FO specifications in a leader election protocol as well as for paper assignment in a conference mangagement system to exclude unappreciated disclosure of reports.