Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Specification sketching for Linear Temporal Logic


Neider,  Daniel
Group R. Majumdar, Max Planck Institute for Software Systems, Max Planck Society;


Roy,  Rajarshi
Group R. Majumdar, Max Planck Institute for Software Systems, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Preprint), 345KB

Supplementary Material (public)
There is no public supplementary material available

Lutz, S., Neider, D., & Roy, R. (2022). Specification sketching for Linear Temporal Logic. Retrieved from https://arxiv.org/abs/2206.06722.

Cite as: https://hdl.handle.net/21.11116/0000-000A-BF32-7
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.