# Specification Patterns for Robotic Missions

arXiv: https://arxiv.org/abs/1901.02077 · HTML: https://mlsanity.com/paper/1901.02077/

## Key facts

- Cited by 16 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jan 2019.

## Built on by (most cited first, 16 of 16)

- [Plug in the Safety Chip: Enforcing Constraints for LLM-driven Robot Agents](https://mlsanity.com/paper/2309.09919/) (2023)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [SPINE: Online Semantic Planning for Missions with Incomplete Natural Language Specifications in Unstructured Environments](https://mlsanity.com/paper/2410.03035/) (2024)
- [Verifiably Following Complex Robot Instructions with Foundation Models](https://mlsanity.com/paper/2402.11498/) (2024)
- [From explanation to synthesis: Compositional program induction for learning from demonstration](https://mlsanity.com/paper/1902.10657/) (2019)
- [Neural Reward Machines](https://mlsanity.com/paper/2408.08677/) (2024)
- [Ground-Compose-Reinforce: Grounding Language in Agentic Behaviours using Limited Data](https://mlsanity.com/paper/2507.10741/) (2025)
- [Constrained Decoding for Safe Robot Navigation Foundation Models](https://mlsanity.com/paper/2509.01728/) (2025)
- [Logically Constrained Robotics Transformers for Enhanced Perception-Action Planning](https://mlsanity.com/paper/2408.05336/) (2024)
- [Pretrained Embeddings as a Behavior Specification Mechanism](https://mlsanity.com/paper/2503.02012/) (2025)
- [Supervised Bayesian Specification Inference from Demonstrations](https://mlsanity.com/paper/2107.02912/) (2021)
- [Fully Learnable Neural Reward Machines](https://mlsanity.com/paper/2509.19017/) (2025)
- [INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations](https://mlsanity.com/paper/2503.13660/) (2025)
- [DeepDFA: Injecting Temporal Logic in Deep Learning for Sequential Subsymbolic Applications](https://mlsanity.com/paper/2602.03486/) (2026)
- [Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications](https://mlsanity.com/paper/2604.18228/) (2026)
- [Coherency through formalisations of Structured Natural Language, A case study on FRETish](https://mlsanity.com/paper/2605.10462/) (2026)

## Abstract (arXiv)

Mobile and general-purpose robots increasingly support our everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing their complex behaviors known as missions. Recognizing the need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation, or guiding the implementation. For instance, the logical language LTL is commonly used by experts to specify missions, as an input for planners, which synthesize the behavior a robot should have. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems, each of which detailing the usage intent, known uses, relationships to other patterns, and---most importantly---a template mission specification in temporal logic. Our tooling produces specifications expressed in the LTL and CTL temporal logics to be used by planners, simulators, or model checkers. The patterns originate from 245 realistic textual mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios we defined with two well-known industrial partners developing human-size robots. We validated our patterns' correctness with simulators and two real robots.
