Home

Welcome to the LTL_stack wiki! This stack consists of three packages that you can use with ROS to execute provably-correct robot controllers. Please follow the instructions below to execute controllers synthesized from LTL with ROS.

If you are interested in the theoretical portion of the work, you can refer to this paper[1].

[1] Kai Weng Wong, Hadas Kress-Gazit, From High-level Task Specification to Robot Operating System (ROS) Implementation. IEEE International Conference on Robotic Computing (IRC2017). Taichung, Taiwan. 2017.

Dependencies

You need the following dependencies to run LTL_stack:

• slugs: Download and compile this version of slugs.
  • This is the patching_multiRobot branch in the repo, not the master branch or the official master branch.
  • Instructions:
    1. Compile slugs by running make in the 'slugs/src' directory.
    2. Make sure slugs can be found anywhere by adding this line export PATH=$PATH:</path/to/slugs_src_folder> to your ~/.bashrc file. Replace </path/to/slugs_src_folder> with the path to your slugs/src folder.
• Tkinter:sudo apt-get install python-tk

Tutorials

A. Try an example

B. Writing a proposition node

C. Generating A New Example

Other Useful Information

• Package Overview
• Proposition YAML File: YAML file that specifies the correspondence of each proposition to a ROS file/program.
• Setup Launch YAML File: YAML file needed to automatically generate launch files.