ReSpeC

Reactive Specification Construction kit

About

ReSpeC (respec) is a Python framework for constructing Linear Temporal Logic (LTL) formulas and composing reactive LTL specifications for use in the synthesis of high-level robot controllers (aka reactive mission plans).

ReSpeC was first used in Team ViGIR's Behavior Synthesis ROS stack to generate LTL specifications for an ATLAS humanoid robot, in the context of the 2015 DARPA Robotics Challenge (DRC).

What ReSpeC is NOT meant for:

• It is not an executive for high-level robot control. For that, see LTLMoP, SMACH, and FlexBE.
• It is not a structured or natural language parser for robotics. For that, see LTLMoP and SLURP.
• It does not have a graphical user interface. For that, see LTLMoP and the FlexBE app.
• It does not synthesize a robot controller (finite-state machine). However, its output can be readily used with the slugs GR(1) synthesizer. Also see gr1c and openpromela.

Maintainers:

• Spyros Maniatopoulos (@spmaniato, sm2296@cornell.edu)

Examples

• Run python examples/atlas_specification.py. You will see LTL terminal output.
• More examples of both individual formulas and full specifications coming soon!

Documentation

Read the Docs coming soon!

Publications

coming soon!

License

BSD-3 (see LICENSE file)