# Item

ITEM ACTIONSEXPORT

Released

Paper

#### Specification sketching for Linear Temporal Logic

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

arXiv:2206.06722.pdf

(Preprint), 345KB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

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

##### Abstract

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.

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.