Task specifications - VerifiableRobotics/LTLMoP GitHub Wiki

Overview

Task specifications dictate what the robot must do (\phi_s), as well as any assumptions that can be made about the behavior of the environment (\phi_e).

Both of these parts of the specification are composed of initial conditions, safety properties (things that must always [never] hold), and goals (things that must happen infinitely often).

Specifications can be written in several languages, depending on the parsing pipeline that is chosen.

LTL Form

This results in an overall specification of the form: \phi = (\phi_e^i \land \phi_e^t \land \phi_e^g \Rightarrow \phi_s^i \land \phi_s^t \land \phi_s^g)

• TODO: latexify
• TODO: cite gr(1)
• TODO: special interpretation of system initial conditions

Supported Language Pipelines

• [Structured English](Structured English Parser)
• A small subset of natural language via SLURP
• [Raw LTL](Raw LTL Specification Parser)