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.

Versions

• Standalone: running without ROS
• ROS: running with ROS

System Requirements

The current repo works on

• Mac (standalone version)
• Ubuntu (standalone version and ROS version).

Dependencies

You need the following dependencies to run LTL_stack:

• slugs: Download and compile this version of slugs with the following command:
  • git clone -b LTL_stack https://git@github.com/wongkaiweng/slugs.git
  • This is the LTL_stack branch in the repo, not the master branch or the official master branch.
  • Instructions:
    1. Install boost
       • Mac - brew : brew install boost. See link.
       • Mac - MacPorts: sudo port install boost. See link.
       • Ubuntu: sudo apt-get install libboost-all-dev. See link.
    2. Compile slugs by running make in the 'slugs/src' directory.
    3. 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 (ROS version)

A. Try an example

B. Write a proposition node

C. Start only the controller(automaton) executor

D. Create a new example

Tutorials without ROS (standalone version)

Step by step Execution Guide with SLUGS and SLUGS Monitor

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.