Examples - VerifiableRobotics/LTLMoP GitHub Wiki

Here is a list of robot mission examples for LTLMoP. All examples are located in the src/examples folder. The folder src/examples/testing contains examples for developers only.

Table of Contents

• ScareTheRobot
• FireFighting
• FollowInLTL
• Grocery
• HideAndSeek
• CleanRooms
• LineFollower
• DeliverMeals
• slurp_unsynth
• unsynth

For this mission the Spider robot will walk across the field and go scare the Nao robot. The spider robot will start under a box and will start to move once the box is removed. The spider will utilize different walking gaits based on the terrain it is currently working through. Once the spider robot get into the region where the Nao robot locates, the spider robot will perform predefined actions. The Nao robot will react in response.

• Different walking gaits of the spider robot to allow it pass through more complex terrains.
• The ability to utilize sensing and actuation from multiple robots simultaneously.

For this example, the robot acts as a firefighter in a simple household environment. The mission of the robot is to search the whole house, and bring any detected hazardous item to the porch region. In addition, if the robot detects a person, it needs to stay in place and radio for help.

• The ability to specify picking up, carrying and dropping an item
• The ability to refer to multiple regions with a group name and quantifiers.
• The ability to give a mission specification in LTL formulas. (SpecInLTL.spec)

• Cameron Finucane, Gangyuan Jing, Hadas Kress-Gazit: LTLMoP: Experimenting with language, Temporal Logic and robot control. IROS 2010: 1988-1993

In this example, the robot is asked to follow a moving target in a predefined environment. What "follow" means in this scenario is to always end up in the same region as the target, but stay in place if the target is constantly moving.

• The ability to give a mission specification in LTL formulas.
• The ability to specify the "follow" behavior
• An unsynthesizable specification if the robot is asked to never go to some regions that the target might go

For this example, the robot acts as an employee in a simple grocery store environment. The mission of the robot is to patrol around the store, and report to the manager if there is any missing item from the shelf. In addition, if the robot detects a spill on the aisles, it needs to avoid that aisles.

• The ability to keep track the status of the environment (spills)
• An unsynthesizable specification if no behavior is specified for the situation when all aisles have spills.

• Gangyuan Jing, Cameron Finucane, Vasumathi Raman, Hadas Kress-Gazit: Correct high-level robot control from structured English. ICRA 2012: 3543-3544

The robot starts in the parking lot. If it is a seeker, it will stay there and count until it hears a ready whistle. Then the robot will search all the hiding spots until it finds someone. The robot becomes a hider once it found someone. As a hider, the robot will go back to the parking lot and wait for counting to start. Once that happens, the robot will go hide somewhere and whistle.

• A relatively complex real-world example
• The ability to refer to multiple regions with a group name and quantifiers.
• The ability to specify a region with locative propositions.

• Cameron Finucane, Gangyuan Jing, Hadas Kress-Gazit: Designing Reactive Robot Controllers with LTLMoP. Automated Action Planning for Autonomous Mobile Robots 2011

In this example, the robot is asked to go around all regions and search for markers. Once it found a marker, it will first ask the human user for a confirmation. If the human user confirm the action, the robot will pick the marker up and drop it into a designated region.

• The ability to prompt for a confirmation from the human user
• The ability to specify picking up, carrying and dropping an item
• The ability to refer to multiple regions with a group name and quantifiers.

In this example, the robot (NXT) is asked to follow a line on the ground. This example is not suitable for simulation.

• The ability to execute an example without localization of the robot
• The ability to specify the "line follow" behavior

In this example, the robot is asked to go to kitchen, pick up meals and deliver them to region r1 and r2. The robot can carry up to two meals at once.

• The robot will always try to carry as many items as it could.
• The ability to specify picking up, carrying and dropping an item

Three simple examples specified in natural language. All three examples are not synthesizable.

• camera: The robot is asked to both "not activate camera in restricted area" and "always activate your camera"
• follow: The robot is asked to both follow a target and "not go into the kitchen"
• meal: The robot is asked to both deliver meals to all patient rooms and "not go into any public rooms"

• The ability to give a mission specification in natural language.
• Examples of unsynthesizable specifications.

• Daniel J. Brooks, Constantine Lignos, Mikhail S. Medvedev, Ian Perera, Cameron Finucane, Vasumathi Raman, Abraham Shultz, Sean McSheehy, Adam Norton, Hadas Kress-Gazit, Mitchell P. Marcus, Holly A. Yanco: Situation understanding bot through language and environment. HRI 2012: 419-420

Several examples that are not synthesizable. For detailed explanation, please refer to the .spec files

• Examples of unsynthesizable specifications.