ebr-ltl-synth

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.

Download

Docker container

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.

Usage:

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.

Pre-compiled

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.