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.

Package Overview

slugs_ros

This is a wrapper of slugs to send and receive messages with ROS.

controller_executor

You can launch the a controller with slugs easily using this package. The controller node then waits for inputs and outputs to the controller.

rqt_mapping_and_analysis

This package provides a graphical user interface (GUI) for users to map inputs and outputs of the controller to ROS nodes. The GUI also provides suggestions to modify the specification.

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

1. Download the repo into your workspace src folder: git clone https://github.com/VerifiableRobotics/LTL_stack.git
2. catkin_make your workspace to make sure LTL_stack can be found.
3. Make sure the files in LTL_stack are all executable: find ~/LTL_stack -type f -exec chmod 755 {} \;
4. Try a simple example by running roslaunch controller_executor tutorial_all.launch. You should see windows below.
5. Click the run_executor button to start execution (The button turns green). Turtlesim should start spinning.
6. Now if you click the sense_object button (The button turns green), Turtlesim should stop. Green is True and Red is False here. The grey box indicates the values of each proposition.
7. You are done! If you want to know more about what each file is doing, you can find more information below.

What's in the example folder

File	Description
setup_launch_tutorial.yaml	Config file to automatically generate all the launch files.
tutorial.slugsin	LTL specification in slugs format.
tutorial.yaml	Define how each proposition corresponds to a ROS file. It also specifies the topic of each proposition.
tutorial_background.launch	Launch nodes other than proposition nodes.
tutorial_executor.launch	Take in the LTL specification, synthesize a controller and execute it with slugs.
tutorial_propositions.launch	Launch all the proposition files as defined in simple.yaml.
tutorial_all.launch	Launch all the other launch files in the folder. An easy way to start running the example.

Other Useful Information

• Proposition YAML File: YAML file that specifies the correspondance of each proposition to a ROS file/program.
• Setup Launch YAML File: YAML file needed to automatically generate launch files.
• How do you generate another example easily