# Specification sketching for Linear Temporal Logic

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 39 references that are in the map.
- First posted on arXiv 14 Jun 2022.

## Builds on (most cited first, 3 of 3)

- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [The Complexity of Learning Linear Temporal Formulas from Examples](https://mlsanity.com/paper/2102.00876/) (2021)
- [Learning Interpretable Models in the Property Specification Language](https://mlsanity.com/paper/2002.03668/) (2020)

## Abstract (arXiv)

Virtually all verification and synthesis techniques assume that the formal specifications are readily available, functionally correct, and fully match the engineer's understanding of the given system. However, this assumption is often unrealistic in practice: formalizing system requirements is notoriously difficult, error-prone, and requires substantial training. To alleviate this severe hurdle, we propose a fundamentally novel approach to writing formal specifications, named specification sketching for Linear Temporal Logic (LTL). The key idea is that an engineer can provide a partial LTL formula, called an LTL sketch, where parts that are hard to formalize can be left out. Given a set of examples describing system behaviors that the specification should or should not allow, the task of a so-called sketching algorithm is then to complete a given sketch such that the resulting LTL formula is consistent with the examples. We show that deciding whether a sketch can be completed falls into the complexity class NP and present two SAT-based sketching algorithms. We also demonstrate that sketching is a practical approach to writing formal specifications using a prototype implementation.