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.

System Requirements

The current repo works on *Mac (tested without ROS) *Ubuntu (tested with/without ROS).

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 with ROS

A. Try an example

B. Write a proposition node

C. Start only the controller(automaton) executor

D. Create a new example

Tutorials without ROS (SLUGS only)

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.