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.

Docker container

We provide a container that can be run on any platform with Docker installed. This is the download link for the tarball containing a README file, the script for running the container, a set of examples, and the LICENSE.

Usage:

Ensure that you have installed Docker ≥ 19. To see the help message, run from your terminal: 

      
$ bash ebr-ltl-synth.sh -h

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

Example:

You can find a lot of examples inside the `./examples` directory. You can try for example to test the realizability of the following formula: 

X(!u | !c) & X(!u | c)

INPUT : u
OUTPUT : c
by executing: 
$ bash ebr-ltl-synth.sh -smv -b demiurge examples/smv/test10.smv

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 and can be used to reproduce the results on the above-mentioned paper.

Contacts