Created: 2014-05-19 10:34
Updated: 2014-06-26 21:35

Guarded Parameterized Bounded Synthesis

This prototype for the synthesis of guarded systems is based on the Party tools by Ayrat Khalimov, Swen Jacobs, and Roderick Bloem. Please also read


  • python3
    • python-graph-core
  • Z3 4.3.1 with API for python
  • ltl3ba 1.0.2

Directory Structure

  • The src directory contains the implementation.
  • The benchmarks directory includes example LTL specification files.


Please set the paths for the required tools (Z3, lzl3ba) in

Run the Prototype

  • Run python3 --help in order to get further information about how to run the program

Example Setup (tested on Debian wheezy)

  1. Create folder structure

    mkdir -p gp_bosy/utils
    mkdir -p gp_bosy/guardedsynthesis  # clone repository...
  2. Install required packages from Debian repository

    sudo apt-get install build-essential libbdd-dev python3 python3-pip
  3. Build z3

    1. Move to the utils directory
    2. Install the newest git version [2]
    3. Checkout the unstable branch of z3 and start the build [3]
  4. Build ltl3ba

    cd utils
    tar xzf ltl3ba-1.0.2.tar.gz
    cd ltl3ba
    cd ..
  5. Get required python packages

    pip3 install python-graph-core
  6. Set paths in

  7. Start our prototype

    PYTHONPATH=$PYTHONPATH:/some_path/utils/z3/build/ python3

    Setting the PYTHONPATH is only necessary if you did not install z3.

    Example call: python3 -t conjunctive_guards --min-bound 2 2 --max-increments 5 --instances 1 5 specification.ltl

    • Disjunctive system with 2 templates
    • 1 instances of the first template
    • 5 instances of the second template
    • Template sizes are at least (2,2) and at most (7,7)


Guarded Parameterized Bounded Synthesis implemented by Simon Ausserlechner based on the Parameterized Bounded Synthesis tool by Ayrat Khalimov, Swen Jacobs, Roderick Bloem, TU Graz.


Free for any use with references to the original authors.





Cookies help us deliver our services. By using our services, you agree to our use of cookies Learn more