This repository contains a collection of benchmarks used in different papers for infinite-state reactive synthesis and infinite-state game solving. This collection will grow over time and is by no means complete at the moment. If you would like to contribute some benchmarks or have question regarding them make a pull request, issue, or write me an E-Mail.
The current benchmark files where created in the following papers:
- Benedikt Maderbacher, Roderick Bloem: Reactive Synthesis Modulo Theories using Abstraction Refinement, FMCAD 2022. Remark: The files here have a different format, a script exists to translate them back.
- Philippe Heim, Rayna Dimitrova: Solving Infinite-State Games via Acceleration, POPL 2024
- Anne-Kathrin Schmuck, Philippe Heim, Rayna Dimitrova, Satya Prakash Nayak: Localized Attractor Computations for Infinite-State Games, CAV 2024
- Philippe Heim, Rayna Dimitrova: Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis, POPL 2025
Note that the specific benchmark idea might come from a different sources.
More benchmarks can be found in the sweap repository, and will hopefully be soon integrated here.