A reactive synthesis tool for the Extended Bounded Response fragment of Linear Temporal Logic, based on the paper:
Cimatti, A., Geatti, L., Gigante, N., Montanari, A., & Tonetta, S. (2020). Reactive Synthesis from Extended Bounded Response LTL Specifications. TU Wien Academic Press.
In addition, we provide a container that can be run on any platform with Docker installed. This is the download link for the script for running the container.
Ensure that you have installed Docker ≥ 19.
USAGE
ebr-ltl-synth [-smv | -tlsf] -b [demiurge | safetysynth] [-s] <file>
OPTIONS
-smv The input file is in SMV format
-tlsf The input file is in TLSF format
-b The backend used for solving safety games
('demiurge' or 'safetysynth')
-s Synthesize a strategy if the specification is realizable
Note: the first time you run the script, it may take some time because Docker has to download the image from Docker Hub.
A version of the tool compiled for CentOS 7 can be download at this link. It has been tested to work on the StarExec platform for the SYNTCOMP community.