Specification sketching for Linear Temporal Logic

Simon Lutz1 Daniel Neider2 Rajarshi Roy

Lutz et al.

Technical University of Kaiserslautern, Kaiserslautern, Germany Max Planck Institute for Software Systems, Kaiserslautern, Germany

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.

§ INTRODUCTION

Due to its unique ability to prove the absence of errors mathematically, formal verification is a time-tested method of ensuring the safe and reliable operation of safety-critical systems.
Success stories of formal methods include application domains such as communication system [13, 25], railway transportation [2, 3],
aerospace [16, 9], and operating systems [37, 21] to name but a few.

However, there is an essential and often overlooked catch with formal verification: virtually all techniques assume that the specification required for the design or verification of a system is available in a suitable format, is functionally correct, and expresses precisely the properties the engineers had in mind.
These assumptions are often unrealistic in practice.
Formalizing system requirements is notoriously difficult and
error-prone [5, 28, 33].
Even worse, the training effort required to reach proficiency with specification languages can be disproportionate to the expected benefits [10], and the use of formalisms such as temporal logics require a level of sophistication that many users might never develop [19].

We address this severe, practical issue by introducing a fundamentally novel approach to writing formal specifications, named specification sketching.
Inspired by recent advances in automated program synthesis [35, 36], our new paradigm allows engineers to express their high-level insights about a system in terms of a partial specification, named specification sketch, where parts that are difficult or error-prone to formalize can be left out.
Moreover, the engineer is asked to provide example executions of the system that the specification should allow or forbid.
Based on this additional data, a so-called sketching algorithm then fills in the missing low-level details to obtain a complete specification.

While the concept of specification sketching is conceivable for a wide range of specification languages, we here focus on Linear Temporal Logic (LTL) [29].
The rationale for this choice is twofold.
First, LTL is popular in academia and widely used in industry [15, 16, 18], making it the de facto standard for expressing (temporal) properties in verification and synthesis.
Second, LTL is well-understood and enjoys good algorithmic properties [8, 29].
Furthermore, its intuitive and variable-free syntax have recently prompted efforts to adopt LTL (over finite words) also in artificial intelligence (e.g., to specify reward functions in reinforcement learning [6]).

In the context of specification sketching for LTL, a sketch can leave logical operators or even entire subformulas unspecified, while examples are ultimately-periodic words.
To illustrate this setting, let us consider the request-response property $P$ expressing that every request $p$ has to be answered eventually by a response $q$.

This property can be formalized by the LTL formula $\varphi \coloneqq \lglobally (p \rightarrow \lnext \leventually q)$, which uses the standard temporal modalities $\leventually$ (“finally”), $\lglobally$ (“globally”), and $\lnext$ (“next”).
However, let us assume for the sake of this example that an engineer is unsure how to formalize $P$.
In this situation, our sketching paradigm allows the engineer to express high-level insight in the form of a sketch, say $\lglobally (p \rightarrow {\placeholder})$, where the question mark indicates which part of the specification is missing.
Additionally, the engineer provides two examples:

* a positive (infinite) trajectory $(\{ p\} \{ q \})^\omega$, expressing that $q$ is the response that should be used to answer a request, and

* a negative (infinite) trajectory $\{ q \}^\omega$, intended to disallow the system to send responses without requests.

Our sketching algorithm then computes a substitution for the question mark such that the completed LTL formula is consistent with the examples (e.g., $\lnext \leventually q$).
We set up all necessary definitions in Section <ref> and formally define LTL sketching in Section <ref>.

It turns out that it is not always possible to find a substitution that is consistent with the given examples (see Example <ref> on Page eg:formula-non-existence).
However, we show in Section <ref> that the problem of deciding whether such a substitution exists is in the complexity class .
Moreover, we develop an effective decision procedure that reduces the original question to a satisfiability problem in propositional logic.
This reduction permits us to apply highly-optimized, off-the-shelf SAT solvers to check whether a consistent substitution exists.

In Section <ref>, we develop two sketching algorithms for LTL.
The first algorithm uses the decision procedure of Section <ref> as a sub-routine and transforms the sketching problem into a series of LTL learning problems (i.e., in problems of learning an LTL formula—without syntactic constraints—from positive and negative examples).
This transformation allows us to apply a diverse array of learning algorithms for LTL, which have been proposed during the last five years [27, 7, 31].
Our second sketching algorithm, on the other hand, extends the LTL learning algorithm by Neider and Gavran [27] and uses a SAT-based technique as an effective means to search for solutions of increasing size.

Finally, Section <ref> presents an empirical evaluation with a prototype implementation, named .
We observed that our algorithms are effective in completing a variety of sketches having different missing information.
Further, comparing our algorithms, we concluded that our second algorithm outperforms our first algorithm in terms of running time and size of the solution.
We conclude this paper in Section <ref> with a discussion of promising directions for future work.

§.§.§ Related Work

The general idea of allowing partial specifications is not entirely new, but it has not yet been investigated as general as in this work.
The most similar setting is one in which templates are used to mine temporal specifications from system executions.
In this context, a template is a partial formula, similar to a sketch.
However, unlike a sketch, a template is typically completed with single atomic propositions or simple formulas, usually without temporal modalities (e.g., restricted Boolean combinations of atomic propositions).
An example of this approach is Texada [22, 23], a specification miner for LTLf formulas (i.e., LTL over finite horizon).
Texada accepts an arbitrary template (property type in their terminology) and a set of system executions as input and completes the template with atomic propositions such that the resulting LTL formula satisfies all of the system executions.
Since LTLf (and LTL for that matter) is defined over a finite, user-provided set of atomic propositions, there are only finitely many ways to fill in the missing parts of a template, and Texada amounts to a search over this finite search space.
By contrast, our approach can complete a sketch with complex LTL formulas and, hence, has to search in an infinite space.

Various other techniques operate in settings where the templates are even more restricted.
For example, Li et al. [24] mine LTL specification based on templates from the GR(1)-fragment of LTL (e.g., $\lglobally\leventually\placeholder$, $\lglobally(\placeholder_1 \rightarrow \lnext\placeholder_2)$, etc.), while Shah et al. [34] mine LTL formulas that are conjunctions of a set of common temporal properties as identified by Dwyer et al. [11].
In addition, the work by Kim et al. [20] uses a set of interpretable LTL templates, widely used in the development of software systems, to obtain LTL formulas robust to noise in the input data.
In the context of CTL, on the other hand, Wasylkowski and Zeller [38] mine specifications using templates of
the form $\mathbf{A} \leventually \placeholder$, $\mathbf{A} \lglobally(\placeholder_1 \rightarrow \leventually\placeholder_2)$.
However, all of the works above complete the templates only with atomic propositions (and their negations in some cases).

Another setting is the one in which general (and complex) temporal specifications are learned from system executions without any constraint on the structure of the specification.
The most notable work in this setting is that by Neider and Gavran [27], who learn LTL formulas from system executions using a SAT solver.
Similar to their Neider and Gavran is the work by Camacho et al. [7], which proposes a SAT-based learning algorithm for LTLf formulas via Alternating Finite Automata as an intermediate representation.
Raha et al. [30] present a scalable approach for learning formulas in a fragment of LTLf without the $\luntil$-operator, while Roy, Fisman, and Neider [32] consider the Property Specification Language (PSL).
However, none of these works can exploit insights about the structure of the specification to aid the learning mining process.

Finally, it is worth mentioning that LTL sketching can be seen as a particular case of syntax-guided synthesis, where syntactic constraints on the resulting formulas are expressed in terms of context-free grammars.
While this approach is more expressive in that it also allows restricting the syntax of the formulas that can be used to fill in missing parts of a sketch, we are convinced that the concept of sketching is more natural and intuitive, and it allows for efficient algorithms.
An example of a syntax-guided approach is SySLite [1], a CVC4-based tool for learning Past-time LTL (over finite executions).
However, we are unaware of any syntax-guided algorithm for our setting: learning LTL formulas over infinite executions.

§ PRELIMINARIES

We now formally introduce the basic notions that are used throughout the paper.

§.§.§ Finite and Infinite Words

To model trajectories of a system, we use the notion of words over an alphabet that represents the system events.
Formally, an alphabet $\Sigma$ is a nonempty, finite set.
The elements of this set are called symbols.
A finite word over an alphabet $\Sigma$ is a sequence $u = a_0 \dots a_n$ of symbols $a_i \in \Sigma$ for $i \in \{0, \dots, n\}$.
The empty sequence, referred to as empty word, is denoted by $\varepsilon$.
The length of a finite word $u$ is denoted by $|u|$, where $|\epsilon| = 0$.
Moreover, $\Sigma^*$ denotes the set of all finite words over the alphabet $\Sigma$, while $\Sigma^+$ = $\Sigma^* \setminus \varepsilon$ is the set of all non-empty words.

An infinite word over $\Sigma$ is an infinite sequence $\alpha = a_0 a_1 \dots$ of symbols $a_i \in \Sigma$ for $i \in \nat$.
We denote the $i$-th symbol of an infinite word $\alpha$ by $\alpha[i]$ and the finite infix of $\alpha$
from position $i$ up to (and excluding) position $j$ with $\alpha[i,j)=a_i a_{i+1}\cdots a_{j-1}$.
We use the convention that $\alpha[i,j)=\varepsilon$ for any $i\geq j$.
Further, we denote the infinite suffix starting at position $j\in \nat$ by $\alpha[j,\infty)=a_j a_{j+1} \cdots$.
Given $u \in \Sigma^+$, the infinite repetition of $u$ is the infinite word $u^{\omega} = uu \dots \in \Sigma^{\omega}$.
An infinite word $\alpha$ is called ultimately periodic if it is of the form $\alpha = uv^{\omega}$ for a $u \in \Sigma^\ast$ and $v \in \Sigma^+$.
Finally, $\Sigma^{\omega}$ denotes the set of all infinite words over the alphabet $\Sigma$.

§.§.§ Propositional Boolean Logic

Since the presented algorithms rely on the Satisfiability (SAT) problem, as a prerequisite, we introduce Propositional Logic.
Let $Var$ be a set of propositional variables, which take Boolean values from $\mathbb{B} = \{0,1\}$ (0 representing $\lfalse$ and 1 representing $\ltrue$).
Formulas in propositional (Boolean) logic—which we denote by capital
Greek letters—are inductively constructed as follows:

* each $x \in Var$ is a propositional formula; and

* if $\Psi$ and $\Phi$ are propositional formulas, so are $\lnot \Psi$ and $\Psi \lor \Phi$.

Moreover, we add syntactic sugar and allow the formulas $\ltrue$, $\lfalse$, $\Psi \land \Phi$,$\Psi \Rightarrow \Phi$, and $\Psi \Leftrightarrow \Phi$, which are defined as usual.
A propositional valuation is a mapping $v : \mathit{Var} \to \mathbb{B}$, which maps propositional variables to Boolean values.
The semantics of propositional logic is given by a satisfaction relation $\models$ that is inductively defined as follows: $v \models x$ if and only if
$v(x) = 1, v \models \lnot\Phi$ if and only if $v \nvDash \Phi$, and $v \models \Psi \lor \Phi$ if and only if $v \models \Psi$ or $v \models \Phi$.
In the case that $v \models \Phi$, we say that $v$ satisfies $\Phi$ and call it a model of $\Phi$.
A propositional formula $\Phi$ is satisfiable if there exists a model $v$ of $\Phi$.
The size of a formula is the number of its subformulas (as defined in the usual way).
The satisfiability problem of propositional logic is the problem of deciding whether a given formula is satisfiable.
Although this problem is well-known to be NP-complete, modern SAT solvers implement optimized decision procedures that can check satisfiability of formulas with millions of variables [4].
Moreover, virtually all SAT solvers also return a model if the input-formula is satisfiable.

§.§.§ Linear Temporal Logic

Linear Temporal Logic (LTL) is a logic to reason about sequences of relevant statements about a system by using temporal modalities.
Formally, given set of propositions $\prop$ that represent relevant statements about the system under consideration,
an LTL formula—which we denote by small Greek letters—is defined inductively as follows:

* each proposition $p \in \prop$ is an LTL formula; and

* if $\psi$ and $\varphi$ are LTL formulas, so are $\lnot \psi$, $\psi \lor \varphi$, $\lnext \psi$ (“neXt”), and $\psi \luntil \varphi$ (“Until”).

As syntactic sugar, we allow the formulas
$\ltrue$, $\lfalse$, $\psi \land \varphi$ and $\psi \rightarrow \varphi$, which are defined as usual.
Additionally, we allow the temporal formulas
$\leventually \psi := \ltrue \luntil \psi$ (“Finally”)
and $\lglobally \psi := \lnot \leventually \lnot \psi$ (“Globally”).
Further, we use $\ltlset$ to denote the set of all LTL formulas using.

LTL formulas are interpreted over infinite words $\alpha\in(2^{\prop})^\omega$.
To define how an LTL formula is interpreted on a word, we use a valuation function $V$.
This function maps an LTL formula and a word to a Boolean value and is defined inductively as follows:

\begin{align*}
&V (p, \alpha) = 1 \text{ if and only if } p \in \alpha(0),\\
&V (\lnot \varphi, \alpha) = 1 - V (\varphi, \alpha),\\
&V (\varphi \lor \psi, \alpha) = \max \{V (\varphi, \alpha), V (\psi, \alpha)\},\\
&V (\lnext \varphi, \alpha) = V (\varphi, \alpha[1,\infty))\\
&V (\varphi \luntil \psi, \alpha) = \max_{i \geq 0} \{ \min \{V (\psi, \alpha [i,\infty)), \min_{0 \leq j < i} \{ V (\varphi, \alpha[j,\infty))\}\}\}
\end{align*}

We call $V(\varphi, \alpha)$ the valuation of $\varphi$ on $\alpha$ and say that $\alpha$ satisfies $\varphi$ if $V (\varphi, \alpha) = 1$.

[Syntax Tree]

(1) at (0, 0) $\lor$;
(2) at (-.5, -.7) $\luntil$;
(3) at (.5, -.7) $\leventually$;
(4) at (-1.0, -1.4) $p$;
(5) at (-0.5, -1.4) $\lglobally$;
(6) at (-0.5, -2.1) $q$;
(7) at (0.5, -1.4) $\lglobally$;
(8) at (0.5, -2.1) $q$;
[->] (1) – (2);
[->] (1) – (3);
[->](2) – (4);
[->] (2) – (5);
[->] (3) – (7);
[->] (5) – (6);
[->] (7) – (8);

[Syntax DAG]

(1) at (0, 0) $\lor$;
(2) at (-.5, -.7) $\luntil$;
(3) at (.5, -.7) $\leventually$;
(4) at (-1.0, -1.4) $p$;
(5) at (0, -1.4) $\lglobally$;
(6) at (0, -2.1) $q$;
[->] (1) – (2);
[->] (1) – (3);
[->](2) – (4);
[->] (2) – (5);
[->] (3) – (5);
[->] (5) – (6);

Representation of LTL formulas

For a precise representation of LTL formulas, we use syntax trees and syntax DAGs.
Syntax DAGs are directed acyclic graphs (DAG) that one obtains from a syntax tree by merging the common subformulas, providing a canonical representation of LTL formulas.
Figure <ref> illustrates the syntax tree and syntax DAG of the formula $(p\luntil \lglobally q)\lor \leventually\lglobally q$.

The size of an LTL formula $\size{\varphi}$ is defined as the number of its unique subformulas, which corresponds to the number of nodes in the syntax DAG of $\varphi$. For example, the size of the formula $(p\luntil \lglobally q)\lor \leventually\lglobally q$ is 6, as can be seen easily in Figure <ref>.

We denote the set of all LTL operators as $\operators=\prop\cup\unaryOp\cup\binaryOp$.
Here, the propositions are the nullary operators,
$\unaryOp=\{\neg,\lnext,\leventually,\lglobally\}$ are the unary operators and $\binaryOp=\{\lor,\land,\luntil\}$ are the binary operators of LTL.
Further, let $\ltlset$ denote the set of all LTL formulas.

§ PROBLEM FORMULATION

Since the problem of  relies heavily on LTL sketches, we begin with formalizing them first.

§.§.§ LTL Sketch

An LTL sketch is incomplete LTL formulas in which parts that are difficult to formalize can be left out.
The left-out parts are represented using placeholders, denoted by $?$'s as can be seen in Figure <ref>.
We comment on the superscripts on the placeholders in a moment.

(1) at (0, 0) $\placeholder^2$;
(2) at (-.5, -.7) $\luntil$;
(3) at (.5, -.7) $\placeholder^1$;
(4) at (-1.0, -1.4) $\placeholder^0$;
(5) at (0, -1.4) $\lglobally$;
(6) at (0, -2.1) $q$;
[->] (1) – (2);
[->] (1) – (3);
[->](2) – (4);
[->] (2) – (5);
[->] (3) – (5);
[->] (5) – (6);

An LTL sketch

Formally, an LTL sketch $\sketch$ is simply an LTL formula whose syntax is augmented with placeholders.
The placeholders we allow can be of three types:
placeholders of arity zero referred to as Type-0 placeholders, that replace missing LTL formulas;
placeholders of arity one referred to as Type-1 placeholders, that replace missing unary operators;
and placeholders of arity two referred to as Type-2 placeholders, that replace missing binary operators.
In the Figure <ref> (and in the rest of the paper), Type-$i$ placeholders are represented using $?^i$.

Given (possibly empty) sets $\placeholderset^0$, $\placeholderset^1$ and $\placeholderset^2$ consisting of Type-0, Type-1 and Type-2 placeholders, respectively, we define LTL-sketches inductively as follows:

* each element of $\prop \cup \placeholderset^0$ is an LTL-sketch; and

* if $\sketch_1$ and $\sketch_2$ are LTL-sketches, $\unaryvar\sketch_1$ is an LTL-sketch for $\unaryvar\in\unaryOp\cup\placeholderset^1$ and so is $\sketch_1\binaryvar\sketch_2$ for $\binaryvar\in\binaryOp\cup\placeholderset^2$.

Note that an LTL sketch in which $\placeholderset^0=\placeholderset^1=\placeholderset^2=\emptyset$ is simply an LTL formula.
Furthur, let $\placeholderset_{\sketch}=\placeholderset^0\cup\placeholderset^1\cup\placeholderset^2$
denote the set of all placeholders in an sketch $\sketch$.
For the sketch in Figure <ref>, $\placeholderset_\sketch=\{\placeholder^0, \placeholder^1, \placeholder^2\}$.
For brevity, in the rest of the paper, we refer an LTL sketch as a sketch.

The placeholders are abstract symbols that apriori do not have meaning.
To assign meaning to a sketch, we need to substitute all Type-0 placeholders with LTL formulas, all Type-1 placeholders with unary operators and all Type-2 placeholders with binary operators.
We do this using a so-called substitution function (or substitution for short).

Formally, a substitution function $s$ maps placeholders and operators present in a sketch to LTL operators and LTL formulas in such a way that: $s(\placeholder)\in\ltlset$ if $\placeholder\in\placeholderset^0$; $s(\placeholder)\in\Lambda_{U}$ if $\placeholder\in\placeholderset^1$; $s(\placeholder)\in\Lambda_{B}$ if $\placeholder\in\placeholderset^2$; and $s(\lambda)=\lambda$ for any LTL operator $\lambda\in\Lambda$.
Morever, a substitution $s$ is said to be complete for an sketch $\sketch$ if
$s$ is defined for every element in $\Lambda\cup\Pi_{\sketch}$ in $\sketch$.

A complete substitution $s$ can be applied to a sketch $\sketch$ to obtain an LTL formula.
To make this mathematically precise, we define a function $f_s$, which is defined recursively on the structure of $\sketch$ as follows:

\begin{align*}
f_s(\sketch_1  \mathbin{\placeholder^2} \sketch_2) &= f_s(\sketch_1) \mathbin{\circ} f_s(\sketch_2), \text{ where } \circ = s(\placeholder^2);\\
f_s(\mathbin{\placeholder^1} \sketch)) &= \unaryvar f_s(\sketch),\text{ where } \circ=s(\placeholder^1); \text{ and }\\
f_s(\placeholder^0) &= s(\placeholder^0).
\end{align*}

§.§.§ Input sample

While there are many ways to fill a sketch, as alluded in the introduction, we rely on two finite, disjoint sets $P,N \subset (2^{\mathcal{\prop}})^{\omega}$ of ultimately periodic words, such that $P\cap N=\emptyset$.
The words in $P$, referred to as the positive examples, represent the desirable system executions that must be allowed by the resulting specification.
On the other hand, the words in $N$, referred to as the negative examples, represent the undesirable system executions that must be disallowed by the resulting specification.
We call the pair $\sample = (P,N)$ a sample.
Since our sample consists of ultimately periodic words, we assume that they are stored as pairs $(u, v)$ of finite words, where $u \in (2^\prop)^{*}$ and $v \in (2^\prop)^{+}$.
Moreover, let the size of a sample be $|\sample|= \sum\limits_{uv^\omega\in P \cup N} |uv|$.

We say that an LTL formula $\varphi$ is consistent with a sample $\sample = (P,N)$ if $V (\varphi,uv^{\omega}) = 1$ for each $uv^\omega \in P$ (i.e., all positive words satisfy $\varphi$) and $V(\varphi,uv^{\omega}) = 0$ for each $uv^\omega \in N$ (i.e., all negative examples do not satisfy $\varphi$);

§.§.§ The LTL sketching problem

Having defined the setting, the main problem that we deal with in the paper is the following:
Given an LTL sketch $\sketch$ and a sample $\sample = (P,N)$, find a complete substitution $s$ for $\sketch$ such that $f_s(\sketch)$ is consistent with $\sample$

Before we address the above (and the more general) problem, let us consider a simpler version of the problem:
Given a sample $\sample = (P,N)$, find a minimal LTL formula $\varphi$ such that $\varphi$ is consistent with $\sample$

The above problem is a restricted version of Problem <ref>, where the sketch $\sketch=\placeholder^0$ (i.e., a single Type-0 placeholder).
Recently, it has attracted a lot of attention in the recent years due to its application in Explainable AI and Specification Mining.
Along with its theoretical analysis [14], there have been a number of efficient algorithms [30, 27, 7] to solve it.

For the  problem, one can always find a solution due to the existence of a generic LTL formula that is consistent with a given sample, as indicated by the following remark:

Given sample $\sample$, there exists an LTL formula $\varphi$ such that $\varphi$ is consistent with $\sample$ and $|\varphi|$ is of size $\mathcal{O}(|S|^4)$.

To construct such a formula, one needs to perform the following two steps.
First, construct formulas $\varphi_{\alpha,\beta}$ for all $\alpha\in P$ and $\beta\in N$, such that $V(\varphi_{\alpha,\beta}, \alpha)=1$
and $V(\varphi_{\alpha,\beta}, \beta) = 0$, using a sequence of $\lnext$-operators and an appropriate propositional formula to describe the first symbol where $\alpha$ and $\beta$ differ.
Second, construct the generic consistent formula $\varphi= \bigvee_{\alpha\in P}\bigwedge_{\beta\in N} \varphi_{\alpha,\beta}$.

For the  problem, however, one may not always find a solution.
This is illustrated using the following example.

Consider the LTL-sketch $\lglobally(\placeholder^0)$ and a sample consisting of a single positive word $\alpha=\{p\}\{q\}^\omega\in P$ and a single negative word $\beta=\{q\}^\omega$.
For this LTL-sketch and sample, there does not exist any substitution that leads to an LTL specification consistent with the sample, which can be shown using contradiction.
Towards contradiction, assume that there exists a specification $\lglobally(\varphi)$ such that $V(\alpha,\lglobally(\varphi))=1$ and $V(\beta,\lglobally(\varphi))=0$.
Based on the semantics of $\lglobally$-operator, $V(\alpha,\lglobally(\varphi))=V(\alpha[1,\infty),\lglobally(\varphi))=1$.
On the other hand, $V(\beta,\lglobally(\varphi))=V(\alpha[1,\infty),\lglobally(\varphi))=0$ since $\beta=\alpha[1,\infty)$ leading to a contradiction.

Since there might not exist any complete substitution for a given LTL sketch and a sample, apriori, it is unclear whether the LTL sketching problem is solvable by any terminating algorithm.
However, we show in Section <ref> that it is indeed possible to find a terminating algorithm for the  problem. Later in Section <ref>, we exploit this result to find suitable substitutions to sketches.

§ EXISTENCE OF A COMPLETE SKETCH

To devise a terminating algorithm for the  problem, we first introduce the related decision problem, which is the following:
Given an LTL-sketch $\sketch$ and a sample $\sample = (P,N)$, does there exist a complete substitution $s$ for $\sketch$ such that $f_s(\sketch)$ is consistent with $\sample$.

In this section, we prove that this problem is indeed decidable and belongs to the complexity class .
Later we also provide a decision procedure based on SAT solving to decide the problem.

§.§ The decidability result

For the decidability result, we introduce some concepts as a preparation. We begin by observing a key property of ultimately periodic words, which is as follows:

Let $uv^\omega \in (2^\prop)^\omega$ and $\varphi$ be an LTL formula.
Then, $uv^\omega[\abs{u} + i, \infty) = uv^\omega[\abs{u} + j, \infty)$ for $j \equiv i \mod \abs{v}$.
Thus, $V(\varphi, uv^\omega[\abs{u} + i, \infty))=V(\varphi, uv^\omega[\abs{u}+j, \infty))$.

Observation <ref> indicates that, for a word $uv^\omega$, there exists only a finite number of distinct suffixes of $uv^\omega$,
all of which originate in the initial $uv$ portion of $uv^\omega$.
We now define the set $\suf{uv^\omega}=\{uv^\omega[i,\infty)~|~ 0\leq i<\abs{uv} \}$ of all (possibly) distinct suffixes of a word $uv^\omega$.
Moreover, we define $\suf{\sample}=\bigcup_{uv^\omega\in(P\cup N)} \suf{uv^\omega}$ to be the set of all suffixes of words in $\sample$.
Observation <ref> further indicates that, to determine the evaluation of an LTL formula $\varphi$ on an ultimately periodic word $uv^\omega$, it is sufficient to determine its evaluation on the initial $\abs{uv}$ suffixes of $uv^\omega$.

Thus, for a compact representation of the evaluation of $\varphi$ on $uv^\omega$, we introduce a table notation $\sattable{\varphi}{uv^\omega}$.
A table $\sattable{\varphi}{uv^\omega}$ is a $\abs{\varphi} \times \abs{uv}$ matrix that consists of the satisfaction of all the subformulas $\varphi'$ of $\varphi$ on the suffixes of $\{uv^\omega\}$.
We define the entries of the matrix as follows:

\begin{align*}
\sattable{\varphi}{uv^\omega}[\varphi',t] = V(\varphi', uv^\omega[t,\infty)) \text{ for all subformulas } \varphi' \text{ of } \varphi \text{ and } 0\leq t < \abs{uv}
\end{align*}

Based on the above definition of the table $\sattable{\varphi}{uv^\omega}$, we identify three properties of these tables.
These properties form important building blocks of the decidability proof (i.e., proof of Theorem <ref>) as we see later.

The first property, which we refer to as Semantic property, is that various rows of table are related to each other in a way that reflects the semantics of LTL.
We formalize a row of a table using the notation $\sattable{\varphi}{uv^\omega}[\varphi', \cdot]$, which refers to the row of $\sattable{\varphi}{uv^\omega}$ corresponding to subformula $\varphi'$.

Let us first demonstrate this property on a running example.
Consider the formula $\psi=p\vee \lnext q$ and the word $\alpha=\{p,q\}\{p\}\{q\}^\omega$.
Figure <ref> illustrates the table $\sattable{\psi}{\alpha}$.
From the figure, one can see that the row $\sattable{\psi}{\alpha}[p\vee \lnext q,\cdot]$ corresponds to the bitwise-OR of the rows $\sattable{\psi}{\alpha}[p,\cdot]$ and $\sattable{\psi}{\alpha}[\lnext q, \cdot]$.

0     1     2

$p$     1     1     0

$q$     1     0     1

$\lnext q$     0     1     1

$p\vee \lnext q$     1     1     1

Bit-vectors for the subformulas of $p\vee \lnext q$

To formalize the relation between the rows corresponding to different subformulas $\varphi'$ of $\varphi$, we must uniquely identify the subformulas.
To this end, given an LTL formula $\varphi$, we assign unique identifiers $i\in\{1,\cdots, n\}$ to each node of the syntax DAG of $\varphi$.
This enables us to denote the subformula of $\varphi$ rooted at Node $i$ with $\varphi[i]$.
For assigning identifiers, we follow the strategy that: we assign the root node with 1; and for every node, we assign an identifier smaller than its children, if it has any.
Note that one can analogously assign labels to syntax DAGs of sketches.
Figure <ref> demonstrates identifiers for the formula $(p\luntil\lglobally q)\land(\leventually(\lglobally q))$.
We further define a function $\ell\colon\{1,\cdots,n\}\mapsto\Lambda$ that maps the identifiers to the corresponding operators in the syntax DAG.

[Syntax DAG ]

(1) at (0, 0) $\land$;
(2) at (-.5, -.7) $\luntil$;
(3) at (.5, -.7) $\leventually$;
(4) at (-1.0, -1.4) $p$;
(5) at (0, -1.4) $\lglobally$;
(6) at (0, -2.1) $q$;
[->] (1) – (2);
[->] (1) – (3);
[->](2) – (4);
[->] (2) – (5);
[->] (3) – (5);
[->] (5) – (6);

(1) at (0, 0) $1$;
(2) at (-.5, -.7) $2$;
(3) at (.5, -.7) $3$;
(4) at (-1.0, -1.4) $4$;
(5) at (0, -1.4) $5$;
(6) at (0, -2.1) $6$;
[->] (1) – (2);
[->] (1) – (3);
[->](2) – (4);
[->] (2) – (5);
[->] (3) – (5);
[->] (5) – (6);

Labeling for formula $(p\luntil\lglobally q)\land(\leventually(\lglobally q))$.

We now describe the set of equations that formalize the relation between the rows.
How a row $\sattable{\varphi}{uv^\omega}[\varphi[i],\cdot]$ corresponding to Node $i$ relates to the others depends the operator $\ell(i)$ in the root node of $\varphi[i]$.
Thus, we list the relation separately for different LTL operators.

If $\ell(i)=p$ for some propostion $p$, then we have the following relation:

\begin{align}\label{eq:prop-table-semantics}
\sattable{\varphi}{uv^\omega}[\varphi[i],t] =
\begin{cases}
1 \text{ if } p\in uv^\omega[t]\\
0 \text{ otherwise}
\end{cases}
\end{align}

If $\ell(i)$ is a unary operator and Node $j$ is the left child of Node $i$, we have the following relations:

\begin{align}
&\text{ if }\ell(i)=\neg:\ \sattable{\varphi}{uv^\omega}[\varphi[i],t] = 1- \sattable{\varphi}{uv^\omega}[\varphi[j],t] \ \text{ for } 0\leq t < \abs{uv}\label{eq:table-relation-neg}\\
&\text{ if }\ell(i)=\lnext:\ \sattable{\varphi}{uv^\omega}[\varphi[i],t] =
\begin{cases}
\sattable{\varphi}{uv^\omega}[\varphi[j],t+1] \ \text{ for } 0\leq t < \abs{uv}-1\\
\sattable{\varphi}{uv^\omega}[\varphi[j],\abs{u}] \ \text{ for } t=\abs{uv}-1
\end{cases}\label{eq:table-relation-next}
\end{align}

While Equation <ref> simply follows from the semantics of $\neg$-operator, Equation <ref> for the $\lnext$-operator exploits Observation <ref> along with its semantics.
In particular, the entry $\sattable{\varphi}{uv^\omega}[\varphi[i],\abs{uv}-1]$ relies on the evaluation of $\varphi[j]$ on $uv^\omega[\abs{u},\infty)$.

If $\ell(i)$ is a binary operator, and Node $j$ and Node $j'$ are the left and right children of Node $i$, respectively, then we have the following relation:

\begin{align}
&\text{ if }\ell(i)=\lor: \sattable{\varphi}{uv^\omega}[\varphi[i],t] = \sattable{\varphi}{uv^\omega}[\varphi[j],t] \lor \sattable{\varphi}{uv^\omega}[\varphi[j'],t] \text{ for } 0\leq t < \abs{uv}\label{eq:table-relation-lor}\\
&\text{ if }\ell(i)=\luntil:\ \sattable{\varphi}{uv^\omega}[\varphi[i],t] = \label{eq:table-relation-until}\\
\bigvee_{t\leq t''<\abs{uv}}\Big[\sattable{\varphi}{uv^\omega}[\varphi[j'],t'']\wedge \bigwedge_{t\leq t'<t''}\sattable{\varphi}{uv^\omega}[\varphi[j],t']\Big] \text{ for } 0\leq t < \abs{u} \nonumber\\
\bigvee_{\abs{u}\leq t''<\abs{uv}}\Big[\sattable{\varphi}{uv^\omega}[\varphi[j'],t'']\wedge \bigwedge_{t'\in t\looparrowright_{u,v} t''}\sattable{\varphi}{uv^\omega}[\varphi[j],t']\Big] \text{ for } \abs{u}\leq t < \abs{uv} \nonumber
\end{cases}
\end{align}

Again, one can see that Equation <ref> follows from the semantics of the $\lor$-operator.
Equation <ref> for the $\luntil$-operator
consists of two cases: the first case provides the relation for entries $t \in \{0,\cdots,\abs{u}-1\}$ in the
initial part u; the second case covers the entries
$t\in\{\abs{u},\cdots,\abs{uv}-1\}$ in the periodic part $v$.
Thereby, the second case uses the periodic nature of $uv^\omega$ to “loop back” into the periodic part $v$ using the set $t\looparrowright_{u,v} t''$ defined as the follows:

\begin{align*}
t \looparrowright_{u,v} t'' =
\begin{cases}
\{t,\cdots, t''-1\}  \text{ if } t < t''; \\
\{\abs{u},\cdots, t''-1, t, \cdots, \abs{uv}-1 \} \text{ if } t'' \leq t
\end{cases}
\end{align*}

Having defined the Semantic property, let us now describe the second property, the Consistency property.
This property ensures that $\sattable{\varphi}{uv^\omega}[\varphi,0]=1$ if and only if $uv^\omega$ satisfies $\varphi$.
Thus, for an LTL formula $\varphi$ consistent with $\sample$, we have the following relation:

\begin{align}\label{eq:table-consistency}
\sattable{\varphi}{uv^\omega}[\varphi,0]=1 \text{ for all } uv^\omega\in P, \text{ and } \sattable{\varphi}{uv^\omega}[\varphi,0]=0 \text{ for all } uv^\omega\in N
\end{align}

The final property we observe is called the Suffix property.
This property originates from the fact that, LTL, being a future-time logic, has the same evaluation on equal suffixes, i.e., $V(\varphi,u_1v_1^\omega[t,\infty)) = V(\varphi,u_2v_2^\omega[t',\infty))$ for $u_1v_1^\omega[t,\infty)=u_2v_2^\omega[t',\infty)$.
Formally, we state the property as follows:

\begin{align}\label{eq:table-suffix-property}
\sattable{\varphi}{u_1{v_1}^\omega}[\varphi,t]=\sattable{\varphi}{u_2{v_2}^\omega}[\varphi,t'] \text{ for all } u_1v_1^\omega[t,\infty)=u_2v_2^\omega[t',\infty)
\end{align}

This property becomes significant later for constructing LTL formulas for Type-0 placeholders.

Having set up the prerequisites, we now proceed to provide an  algorithm to decide the  problem.
For ease of presentation, we demonstrate the algorithm on a simple (but crucial) case in which $\sketch$ consists of only a single Type-0 placeholder $\placeholder^0$.
For this case, one might assume that non-deterministically guessing a substitution for the placeholder should suffice.
However, apriori one does not know the size of the LTL formula that is necessary to substitute the Type-0 placeholder.

Thus, in our $\NP$ algorithm, instead of guessing substitutions, we guess all the entries of the table $\sattable{\sketch}{uv^\omega}$ for each $uv^\omega$ in $\sample$.
Note that the tables have a finite dimension, precisely $\abs{\sketch}\times\abs{uv}$, for each word $uv^\omega$.
Thus, the overall process of simply guessing all the table entries can be done in time $\mathcal{O}({\poly(\abs{\sketch},\abs{\sample})})$.

After guessing the table entries, we must verify that the guessed tables satisfy the three properties, Semantic, Consistency, and Suffix, discussed earlier in this section.
It is easy to verify that checking the first two properties for the tables require time $\mathcal{O}(\poly(\abs{{\sketch}},{\abs{uv}}))$ for each $uv^\omega$ in $\sample$.
For checking the Suffix property, one must identify the equal suffixes in $\suf{\sample}$.
This fact that this can be also done in time $\poly(\abs{\sample})$, is a consequence of Lemma <ref>, stated below.
Intuitively, the result states that two suffixes are equal if they are equal only on a finite portion $b$ of size $\poly(\abs{u_1}, \abs{u_2}, \abs{v_1}, \abs{v_2})$.

$u_1v_1^\omega[t,\infty)=u_2v_2^\omega[t',\infty)$ if and only if $u_1v_1^\omega[t,t+b)=u_2v_2^\omega[t',t'+b)$, where $b=\max(\abs{u_1[t,\abs{u_1})}, \abs{u_2[t',\abs{u_2})})+\lcm(\abs{v_1}, \abs{v_2})$.

First, let us consider $u_1v_1^\omega[t,\infty)=u_2v_2^\omega[t',\infty)$.
Clearly, all prefixes of $u_1v_1^\omega[t,\infty)$ and $u_2v_2^\omega[t',\infty)$ are equal, i.e., $u_1v_1^\omega[t,t+b)=u_2v_2^\omega[t',t'+b)$ for all $b\in\nat$.

For the other direction, we consider $u_1v_1^\omega[t,t+b)=u_2v_2^\omega[t',t'+b)$, for $b=\max(\abs{u_1[t,\abs{u_1})}, \abs{u_2[t',\abs{u_2})})+\lcm(\abs{v_1}, \abs{v_2})$.
Without loss of generality, let us assume that $\abs{u_1[t,\abs{u_1})}\geq\abs{u_2[t',\abs{u_2})}$.
To avoid clutter of notation, we denote $\mu=\abs{u_1[t,\abs{u_1})}$ and $\nu=\lcm(\abs{v_1}, \abs{v_2})$.
Thus, in this case, $b=\mu+\nu$.

The proof, now, is based on two main observations.
First, we begin with the simple observation:

\begin{align*}
u_1v_1^\omega[t,t+\mu) &= u_2v_2^\omega[t',t'+\mu); \text{ and }\\ u_1v_1^\omega[t+\mu,t+b) &= u_2v_2^\omega[t'+\mu,t'+b)
\end{align*}

Second, we have that

\begin{align*}
(u_1v_1^\omega[t+\mu,t+b))^\omega &= v_1^\omega; \text{ and } \\
(u_2v_2^\omega[t'+\mu,t'+b))^\omega &= (v_2^\omega[t'+\mu, t'+\mu+\abs{v_2}))^\omega
\end{align*}

The above observation is due to the fact that $u_1v_1^\omega[t+\mu,t+b) = v_1^{\kappa}$ for $\kappa=\nu/\abs{v_1}$ and $u_2v_2^\omega[t'+\mu,t'+b) = (v_2^\omega[t'+\mu, t'+\mu+\abs{v_2}))^\kappa$ for $\kappa=\nu/\abs{v_2}$.

Now, combining the two observations, we have the following:

\begin{align*}
u_1v_1^\omega &= u_1v_1^\omega[t,t+\mu)\cdot (u_1v_1^\omega[t+\mu,t+b))^\omega\\
&= u_2v_2^\omega[t',t'+\mu)\cdot (u_2v_2^\omega[t'+\mu,t'+b))^\omega\\
&= u_2[t',\abs{u_2}) \cdot u_2v_2^\omega[\abs{u_2}, t'+\mu)\cdot (v_2^\omega[t'+\mu, t'+\mu+\abs{v_2}))^\omega\\
&= u_2v_2^\omega
\end{align*}

We now prove that if the guessed tables satisfy the three properties, then there exists a LTL formula $\psi$ that one can replace in the Type-0 placeholder to obtain a consistent LTL formula.
This fact is asserted by the following theorem.

Let $\sample=(P,N)$ be a sample, $\sketch$ be a sketch with only Type-0 placeholders and tables  $\sattable{\sketch}{uv^\omega}$ be $\abs{\sketch}\times\abs{uv}$ matrices with $\{0,1\}$ entries for each $uv^\omega\in P\cup N$. Then, the following holds: the tables $\sattable{\sketch}{uv^\omega}$ satisfy the Semantic, Consistency and Suffix properties if and only if there exists a substitution $s$ such that LTL formula $f_s(\sketch)$ is consistent with $\sample$.

For simplicity, we again consider that $\sketch$ consists of only one Type-0 placeholder $\placeholder^0$.
The proof can be seemlessly extended to multiple Type-0 placeholders.

For the forward direction, we show the existence of the substitution $s$ by explicit construction of an LTL formula for  $\placeholder^0$.
Towards this, we first construct a sample $\sample'=(P',N')$ as follows:

\begin{align*}
&P'= \{uv^\omega[t,\infty)\in\suf{\sample}~|~\sattable{\sketch}{uv^\omega}[\placeholder^0,t]=1,\ uv^\omega\in P\cup N,\ 0\leq i< \abs{uv}\}\\
&N'= \{uv^\omega[t,\infty)\in\suf{\sample}~|~\sattable{\sketch}{uv^\omega}[\placeholder^0,t]=0,\ uv^\omega\in P\cup N,\ 0\leq i< \abs{uv}\}.
\end{align*}

Since the tables satisfy the Suffix property, we have that $P'\cap N' = \emptyset$.

We can now construct the generic LTL formula $\psi$ consistent with $\sample'$ based on Remark <ref>.
We claim that this formula $\psi$ can be substituted in $\placeholder^0$ to obtain a consistent LTL formula.

Towards this, we first prove that $\sattable{f_s(\sketch)}{uv^\omega}[\psi,\cdot]=\sattable{\sketch}{uv^\omega}[\placeholder,\cdot]$ for all $uv^\omega\in P\cup N$.
To prove this, we exploit two simple observations.
First, using the definition of tables, we have $\sattable{f_s(\sketch)}{uv^\omega}[\psi,t] = V(\psi,uv^\omega[t,\infty))$ for each $uv^\omega[t,\infty)\in\suf{\sample}$.
Second, since $\psi$ is consistent with $\sample'$, we know $V(\psi,uv^\omega[t,\infty))=\sattable{\sketch}{uv^\omega}[\placeholder,t]$.
Together, we have $\sattable{f_s(\sketch)}{uv^\omega}[\psi,t] = \sattable{\sketch}{uv^\omega}[\placeholder,t]$.

Next, we prove that $\sattable{f_s(\sketch)}{uv^\omega}[f_s(\sketch)[i],\cdot]=\sattable{\sketch}{uv^\omega}[\sketch[i],\cdot]$ for each $0\leq i< \abs{\sketch}$ and word $uv^\omega\in P\cup N$. (Note that we denote the same nodes in $f_s(\sketch)$ and $\sketch$ using the same identifiers.)
Towards contradiction, we assume that there exists some $uv^\omega \in P\cup N$ and some $0\leq i< \abs{\sketch}$ and  such that $\sattable{f_s(\sketch)}{uv^\omega}[f_s(\sketch)[i],\cdot]\neq\sattable{\sketch}{uv^\omega}[\sketch[i],\cdot]$.
Let $i^*$ be the maximum row for which the tables become unequal.
The proof, in general, will proceed via a case analysis on the operator $\ell(i^*)$ labeled in Node $i^*$.
However, since for proof is similar for all the operators, we assume $\ell(i)=\neg$ and Node $j^*$ is the left child of Node $i^*$.
Recall that $j^*>i^*$ based on our assignment of identifiers.
Further, based on the Semantic property, $\sattable{f_s(\sketch)}{uv^\omega}[f_s(\sketch)[i^*],t] = 1 - \sattable{f_s(\sketch)}{uv^\omega}[f_s(\sketch)[j^*],t]$ and
$\sattable{\sketch}{uv^\omega}[\sketch[i^*],\cdot]= 1 - \sattable{\sketch}{uv^\omega}[\sketch[j^*],\cdot]$ for each $0\leq t\leq \abs{uv}$ (Equation <ref>).
This implies that $\sattable{f_s(\sketch)}{uv^\omega}[f_s(\sketch)[j^*],\cdot]\neq\sattable{\sketch}{uv^\omega}[\sketch[j^*],\cdot]$, contradicting the maximality of $i^*$.

Finally, observe that $\sattable{f_s(\sketch)}{uv^\omega}[f_s(\sketch),\cdot]=\sattable{\sketch}{uv^\omega}[\sketch,\cdot]$.
As a consequence, since tables $\sattable{\sketch}{uv^\omega}$ satisfy the Consistency property, so does tables $\sattable{f_s(\sketch)}{uv^\omega}$.
This implies that $f_s(\sketch)$ is consistent with $\sample$.

For the other direction, we construct tables $\sattable{\sketch}{uv^\omega}[\psi,\cdot]$ based on the tables $\sattable{f_s(\sketch)}{uv^\omega}[\psi,\cdot]$.
In particular, we have $\sattable{f_s(\sketch)}{uv^\omega}[\psi,\cdot] = \sattable{\sketch}{uv^\omega}[\psi,\cdot]$ for each $0\leq i<\abs{\sketch}$ and $uv^\omega \in P\cup N$.
Since tables $\sattable{f_s(\sketch)}{uv^\omega}[\psi,\cdot]$ satisfy the Semantic, the Consistency and the Suffix properties, so does the tables $\sattable{\sketch}{uv^\omega}[\psi,\cdot]$.

With this, we conclude the  algorithm for the case where $\sketch$ only has one Type-0 placeholder.
We can easily extend the algorithm to the case where $\sketch$ additionally consists of Type-1 and Type-2 placeholders.
In particular, we first guess the operators to be substituted for the Type-1 and Type-2 placeholders and substitute them.
We then obtain a sketch consisting of only Type-0 placeholders.
We can now apply our algorithm that relies on guessing tables, as described above.
In total, we obtain the following result:

The  problem is in $\NP$.

While we determine the complexity upper bound of the  problem to be , the lower bound is open and adds to the list of open problems in the area of LTL inference (see Section 6 of [14]).

§.§ The decision procedure

Based on the  algorithm described above, we now devise a decision procedure to decide the  problem.
The decision procedure relies upon solving an instance of SAT problem to check if there exists suitable tables $\sattable{\varphi}{uv^\omega}$ which satisfy the three properties, discussed in Section <ref>.

To encode entries of the tables, we first introduce the following variables: $y^{u,v}_{i,t}$ for each $i\in\{1, \cdots n\}$, $t\in\{0,\cdots,\abs{uv}-1\}$, and $uv^\omega\in P\cup N$.
A variable $y^{u,v}_{i,t}$ encodes the entry $\sattable{\varphi}{uv^\omega}[\varphi[i],t]$.
Further, to encode the operators to be substituted for the Type-1 and Type-2 placeholders in $\sketch$, we have the following variables:

* $x_{i,\lambda}$ for each Node $i$ where $\ell(i)$ is a Type-1 placeholder and each $\lambda\in\Lambda_{U}$; and

* $x_{i,\lambda}$ for each Node $i$ where $\ell(i)$ is a Type-2 placeholder and each $\lambda\in\Lambda_{B}$

We now impose constraints on the introduced variables to ensure that they encode tables that satisfy the properties for inferring a consistent LTL formula.
We achieve this by constructing a propositional formula $\existFormula$ using the introduced variables.
This formula ensures that the variables $y^{u,v}_{i,t}$ encode tables that satisfy the three required properties.

Since $\existFormula$ ensures the existence of a suitable tables, we have the following property of $\existFormula$: there exists a complete substitution $s$ for $\sketch$ such that $f_s(\sketch)$ is consistent with $\sample$ if and only if $\existFormula$ is satisfiable.
We can now simply check the satisfiability of $\existFormula$ using an off-the-shelf SAT solver to determine the existence of a complete substitution.

Internally, $\existFormula=\Phi^{1,2}_{\placeholder}\wedge\Phi_{\mathit{sem}}\wedge \Phi_{\mathit{con}}\wedge\Phi_{\mathit{suf}}$ is a conjunction of four formulas.
The first conjunct $\Phi^{1,2}_{\placeholder}$ ensures that the Type-1 and Type-2 placeholders are substituted by appropriate operators.
The conjuncts $\Phi_{\mathit{sem}}$, $\Phi_{\mathit{con}}$ and $\Phi_{\mathit{suf}}$ ensure that the variables $y^{u,v}_{i,t}$ encode entries of tables that satisfy the Semantic  property (Equations <ref> to <ref>), the Consistency property (Equation <ref>) and the Suffix property (Equation <ref>), respectively.
We now describe briefly how each of these formulas are constructed.

Constraints for $\Phi^{1,2}_{\placeholder}$.
For each Node $i$ labeled with a Type-1 placeholder (i.e., $\ell(i)\in\placeholderset^1$), we have the following constraint:

\begin{align}\label{eq:selective-label-uniqueness}
\Big[ \bigvee_{\lambda \in \Lambda_{U}} x_{i,\lambda} \Big] \land \Big[ \bigwedge_{\lambda \neq \lambda' \in \Lambda_{U}} \lnot x_{i, \lambda} \lor \lnot x_{i, \lambda'} \Big],
\end{align}

which ensures that the Type-1 placeholder is substituted by a unique unary operator.
For Type-2 placeholders, we have the exact same constraint except that the operators range from the set of binary operators $\Lambda_{B}$.
Now, we construct $\Phi^{1,2}_{\placeholder}$ as the conjunction of all such constraints for the nodes labeled with Type-1 and Type-2 placeholders.

Constraints for $\Phi_{\mathit{sem}}$.
We define $\Phi_{\mathit{sem}} = \bigwedge_{uv^\omega\in P\cup N} \Phi^{u,v}$, where $\Phi^{u,v}$ is a propositional formula that ensures that the
variables $y^{u,v}_{i,t}$ satisfy the Equations <ref> to <ref> for word $uv^\omega$ in $\sample$.
In $\Phi^{u,v}$, for instance, for each Node $i$ labeled with $\lnext$-operator (i.e, $\ell(i)=\lnext$) and has Node $j$ as its left child, we have the following constraint:

\begin{align}\label{eq:semantic}
\Big[\bigwedge_{0\leq t\leq \abs{uv}-1} \Big[ y^{u,v}_{i,t} \leftrightarrow
y^{u,v}_{j,t+1} \Big]\Big] \wedge \Big[y^{u,v}_{i,\abs{uv}-1} \leftrightarrow
\end{align}

This constraints ensures that the variables $y^{u,v}_{i,t}$ satisfy Equation <ref> for the word $uv^\omega$.
We construct similar constraints for the other operators based on their corresponding semantic relation.

For nodes labeled with Type-1 and Type-2 placeholders, we additionally rely on variables $x_{i,\lambda}$ to determine the operator $\lambda$ to be substituted in Node $i$.
For instance, for each Node $i$ labeled with a Type-1 placeholder (i.e., $\ell(i)\in\placeholderset^1$) that has Node $j$ as its left child, we have the following constraint:

\begin{align}\label{eq:placeholder-next-semantics}
x_{i,\lnext} \rightarrow \Big[ \bigwedge_{0\leq t\leq \abs{uv}-1} \Big[ y^{u,v}_{i,t} \leftrightarrow
y^{u,v}_{j,t+1} \Big]\Big] \wedge \Big[y^{u,v}_{i,\abs{uv}-1} \leftrightarrow
\end{align}

The above constraint states that if Node $i$ is substituted with a $\lnext$-operator (i.e., if $x_{i,\lnext}$ is true), the constraint on the $y^{u,v}_{i,t}$ variables is based on Equation <ref>.
We construct similar constraints for when $x_{i,\lambda}$ is true for some other operator $\lambda$ based on the corresponding equation for $\lambda$.
Finally, we construct $\Phi^{u,v}$ as the conjunction of all such constraints that rely on the semantic equations.

Constraints for $\Phi_{\mathit{sem}}$.
We construct $\Phi_{\mathit{con}}$ as follows:

\begin{align}
\Phi_{con} = \Big[\bigwedge_{uv^\omega\in P\cup N} \Phi^{u,v}\Big]\wedge \Big[\bigwedge_{uv^\omega\in P} y^{u,v}_{1,0} \wedge \bigwedge_{uv^\omega\in N} \neg y^{u,v}_{1,0}\Big]
\end{align}

This formula ensures that Equation <ref> is satisfied for the prospective bit-vectors, in addition to ensuring $\Phi^{u,v}$ holds for all $uv^\omega$ in $\sample$.

Constraints for $\Phi_{\mathit{suf}}$.
In $\Phi_{\mathit{suf}}$, for each Node $i$ labeled with a Type-0 placeholder (i.e., $\ell(i)\in\placeholderset^{0}$), we have the following constraint:

\begin{align}\label{eq:suffix}
\bigwedge_{u_1v_1^\omega[t,\infty)=u_2v_2^\omega[t',\infty)\in\suf{\sample}} \Big[ y^{u_1,v_1}_{i,t} \leftrightarrow y^{u_2,v_2}_{j,t'} \Big],
\end{align}

which ensures that the variables $y^{u,v}_{i,t}$ the entries of the tables satisfy Equation <ref>

The following lemma establishes the correctness of the decision procedure.

Let $\sketch$ be a sketch, $\sample$ a sample and $\existFormula$ the formula as defined above. Then,
$\existFormula$ is satisfiable if and only if there exists a complete substitution $s$ such that $f_{s}(\sketch)$ is consistent with $\sample$.

If $\existFormula$ is satisfiable, we can construct a suitable complete substitution $s$ based on the model $v$ of $\existFormula$.
To begin with, for Node $i$ labeled with a Type-1 or Type-2 placeholder $\placeholder$, we have $s(\placeholder) = \lambda$, where $\lambda$ is the unique operator for which $v(x_{i,\lambda})=1$.
Next, for nodes labeled with Type-0 placeholders, we first construct tables $\sattable{\sketch}{uv^\omega}$ for each $uv^\omega\in P\cup N$ using the value of the variables $v(y^{u,v}_{i,t})$.
Based on the construction of $\existFormula$, all of these tables satisfy the Semantic, Consistency and Suffix properties.
Now, we use Lemma <ref> to find substitutions to Type-0 placeholders using the tables $\sattable{\sketch}{uv^\omega}$.

For the other direction, we construct a satisfying assignment $v$ using the substitution function $s$ and tables $\sattable{f_s(\varphi)}{uv^\omega}$ for $uv^\omega\in P \cup N$.
First, we assign $v(x_{i,\lambda}) = 1$ if and only if $s(\placeholder) = \lambda$ for a Node $i$ labeled with a Type-1 or Type-2 placeholder $\placeholder$.
Second, we assign $v(y^{u,v}_{i,t}) = \sattable{f_s(\varphi)}{uv^\omega}[f_s(\sketch)[i],t]$ for each $uv^\omega\in P\cup N$ and $0\leq t\leq |uv|$.
This assignment $v$ satisfies $\Phi^{1,2}_{\placeholder}$, since we obtain $v$ from the syntax DAG of a valid LTL formula.
Further, this assignment satisfies $\Phi_{\mathit{sem}}$, $\Phi_{\mathit{con}}$ and  $\Phi_{\mathit{suf}}$ because the tables satisfy Semantic, Consistency and Suffix properties, respectively, on which the constraints are based.
Overall, $v$ is a model for $\existFormula$.

Finally, we have the following remark to assess the size of the encoding $\existFormula$.

Let $n = \abs{\sketch}$ and $m=\sum_{uv^\omega\in P\cup N} \abs{uv} $.
The formula $\existFormula$ ranges over $\mathcal{O}(n+nm)$ variables and is of size $\mathcal{O}(n + nm^3 + m^2)$.

§ ALGORITHMS TO COMPLETE AN LTL SKETCH

In this section, we describe two novel algorithms for solving the  problem, which aim at searching for concise LTL formulas from sketches.
Our rationale behind finding concise specifications is motivated by two considerations: first, they are more human understandable and thus, easier for the engineers to interpret; second, potentially all verification and synthesis algorithms perform better with smaller specifications.
To this end, our first algorithm relies on existing techniques for learning minimal LTL formulas.
Our second algorithm, alternatively, searches for formulas of increasing size using constraint solving.

§.§ Algorithm based on LTL learning

Our first algorithm for finding concise LTL formulas builds upon the decision procedure for checking the existence of a complete substitution presented in Section <ref>.
In particular, we exploit the formula $\existFormula$ to reduce the  problem to a number of instances of the  problem, one for each Type-0 placeholder.
One can then exploit recent advancements [27, 31] in solving the  problem to find concise ways of filling out the sketch.

Algorithm <ref> outlines the details of the algorithm.
The first step is to construct $\existFormula$ from the given sample and sketch, as described in Section <ref>.
If $\existFormula$ is unsatisfiable, the algorithm straight-away returns that no solution exists (Line <ref>), as established by Theorem <ref>.
If it is satisfiable, we use a model (say $v$) of $\existFormula$, which can be obtained from any off-the-shelf SAT solver, to fill out $\sketch$.
We now describe in detail how to fill out a sketch.

Given a model $v$ of $\existFormula$, in a rather straightforward manner, one can substitute the Type-1 and Type-2 placeholders in $\sketch$ (Line <ref>).
For each Node $i$ where $\ell(i)$ is a Type-1 and Type-2 placeholders, we assign $s(\ell(i))=\lambda$ where, $\lambda$ is the unique operator for which $v(x_{i,\lambda})=1$.

The Type-0 placeholders, however, are more challenging to substitute.
This is because, they represent entire LTL formulas.
Towards substituting Type-0 placeholders, for every Node $i$ where $\ell(i)$ is a Type-0 placeholder (i.e., $\ell(i)\in\placeholderset^0$), we first construct a sample $\sample_i=(P_i,N_i)$ (Line <ref>) as follows:

\begin{align*}
&P_i= \{uv^\omega[t,\infty)\in\suf{\sample}~|~v(y^{u,v}_{1,t})=1\}, \text{ and }\\
&N_i= \{uv^\omega[t,\infty)\in\suf{\sample}~|~v(y^{u,v}_{1,t})=0\}.
\end{align*}

Now, we learn a concise LTL formula $\varphi_i$ consistent with the sample $\sample_i$ (using e.g., algorithms by Neider and Gavran [27]) for substituting $\ell(i)$ (Line <ref>).

Algorithm based on LTL learning

[1]
Input: Sketch $\sketch$, Sample $\sample$
Construct $\existFormula= \Phi^{1,2}_{\placeholder}\wedge \Phi_{\mathit{sem}}\wedge\Phi_{\mathit{con}}\wedge\Phi_{\mathit{suf}}$
$\existFormula$ is satisfiable (say with model $v$)
Substitute Type-1 and Type-2 placeholders in $\sketch$ using $v$
every $i$ such that $\ell(i)\in\placeholderset^0$
Construct $\sample_i=(P_i,N_i)$
Substitute Node $i$ with $\Phi_i$ in $t$
LTL formula does not exist

The correctness of the algorithm is established by the following theorem:

Given sketch $\sketch$ and sample $\sample$,  Algorithm <ref> terminates and completes $\sketch$ to output an LTL formula that is consistent with $\sample$, if such a formula exists.

Observe that Algorithm <ref> constructs new samples for each Type-0 placeholder.
Each of these samples have size $\mathcal{O}(\size{\suf{\sample}})=\mathcal{O}(\size{\sample}^2)$,
which poses a challenge to the scalability of this algorithm.
Furthermore, the new samples are not optimized to produce the minimal possible substitutions.
Our next algorithm improves both on the runtime and the size of the inferred specification.

§.§ Algorithm based on incremental SAT solving

We, now, introduce an algorithm that is based on a series of SAT solving problems, similar to the SAT-based algorithm by Neider and Gavran [27].
Given a sample $\sample$ and a natural number $n\in\nat\setminus\{0\}$, we construct a propositional formula $\incrementalFormula{n}$ of size $\poly(n,\abs{\sample})$ that has the following two properties:

* $\incrementalFormula{n}$ is satisfiable if and only if one can complete $\sketch$ to obtain an LTL formula of size $n$ that is consistent with $\sample$; and

* if $v$ is a model of $\incrementalFormula{n}$, then $v$ contains sufficient information to complete $\sketch$ to construct an LTL formula $\varphi$ of size $n$ that is consistent with $\sample$.

Algorithm based on incremental SAT solving
[1]
Input:  Sketch $\sketch$, Sample $\sample$
Construct $\existFormula= \Phi^{1,2}_{\placeholder}\wedge\Phi_{\mathit{sem}}\wedge\Phi_{\mathit{con}}\wedge\Phi_{\mathit{suf}}$
$\existFormula$ is satisfiable
$n\gets n+1$
Construct $\incrementalFormula{n}= \Phi^{1,2}_{\placeholder}\wedge\Phi^{'}_{\mathit{sem}}\wedge\Phi_{\mathit{con}}\wedge\Phi^{0}_{\mathit{\placeholder},n}$
$\incrementalFormula{n}$ is satisfiable (say with model $v$)
Substitute placeholders in $t$ using $v$
LTL formula does not exist

However, in contrast to the algorithms by Neider and Gavran, we first solve $\existFormula$ (discussed in Section <ref>) to determine the existence of a complete substitution.
If and only if $\existFormula$ is satisfiable, our algorithm checks the satisfiability of $\incrementalFormula{n}$ for increasing values of $n$ (starting from 1) to search for an LTL formula of size at most $n$ that has the same syntactic structure as $\sketch$.
We construct the resulting LTL formula by substituting the placeholders in $\sketch$ based on a model $v$ of the satisfiable formula $\incrementalFormula{n}$.
This idea is illustrated in Algorithm <ref>.

On a technical level, the formula $\incrementalFormula{n}$ is obtained by modifying certain parts of the formula $\existFormula$.
Precisely, $\incrementalFormula{n} =  \Phi^{1,2}_{\placeholder}\wedge\Phi'_{\mathit{sem}}\wedge\Phi_{\mathit{con}}\wedge\Phi^{0}_{\mathit{\placeholder},n}$ employs a two modifications: a new formula $\Phi^{0}_{\mathit{\placeholder},n}$ replaces $\Phi_{\mathit{suf}}$; and $\Phi'_{\mathit{sem}}$ is obtained by adding more constraints to $\Phi_{\mathit{sem}}$.
The formula $\Phi^{0}_{\mathit{\placeholder},n}$ encodes the structure LTL formulas that substitute the Type-0 placeholders.
$\Phi'_{\mathit{sem}}$, again as in $\Phi_{\mathit{sem}}$, ensures that the variables $y^{u,v}_{i,t}$ encode table entries $\sattable{\varphi}{uv^\omega}[\varphi[i],]$ that satisfy Equations <ref> to <ref>.
We now briefly describe the constraints for the newly introduced formulas.

Constraints for $\Phi^{0}_{\mathit{\placeholder},n}$.
The constraints here rely on an additional set of variables:

* $x_{i,\lambda}$ for each Node $i$ labeled with a Type-0 placeholder, and for each $i\in\{\abs{\sketch}+1,\cdots, n\}$ such that $\ell(i)$ is a Type-0 placeholder, and each $\lambda\in\Lambda$; and

* $l_{i,j}$ and $r_{i,j}$ for each Node $i$ labeled with a Type-0 placeholder, and each $i\in\{\abs{\sketch}+1,\cdots,n\}$ and $j\in\{\max(i,\abs{t}),\cdots,n\}$.

The variable $x_{i,\lambda}$, again, encode that Node $i$ is labeled with $\lambda$.
The variables $l_{i,j}$ (and $r_{i,j}$) encode that the left child (and the right child) of Node $i$ is Node $j$.
Together the new variables encode the structure of the prospective LTL formulas for Type-0 placeholders.

We now impose constraints, similar to Constraint <ref>, on the variables $x_{i,\lambda}$ to ensure each node is labeled by a unique LTL operator from $\Lambda$.
Additionally, we ensure that each Node $i$ has a unique left child using the following constraint:

\begin{align}\label{eq:child-uniqueness}
\Big[ \bigvee_{\max(i,\abs{t})\leq j\leq n} l_{i,j} \Big] \land \Big[ \bigwedge_{\max(i,\abs{t})\leq j\neq j'\leq n } \lnot l_{i,j} \lor \lnot l_{i,j'} \Big],
\end{align}

We have a similar constraint to ensure the uniqueness of right child of a node.
Now, we construct $\Psi_{\mathit{str}}$ as the conjunction of all such structural constraints.

Constraints for $\Phi'_{\mathit{sem}}$.
We rely on new variables $y^{u,v}_{i,t}$ for each Node $i$ labeled with a Type-0 variables and each $i\in\{\size{\sketch}+1,n\}$, each $t\in\{0,\cdots,\abs{uv}-1\}$ and each $uv^\omega$ in $\sample$.
On these variables, we impose the following constraint, which is similar to Constraint <ref>:

\begin{align}
\Big[x_{i,\lnext} \wedge l_{i,j}\Big] \rightarrow\bigwedge_{0\leq t\leq \abs{uv}-1} \Big[ y^{u,v}_{i,t} \leftrightarrow
y^{u,v}_{j,t+1} \Big] \wedge \Big[y^{u,v}_{i,\abs{uv}-1} \leftrightarrow
\end{align}

that ensures that the $y^{u,v}_{i,t}$ variables encode entries of table that satisfy Equation <ref>.
We construct $\Phi'_{\mathit{sem}}$ as the conjunction of $\Phi_{\mathit{sem}}$ and the new semantic constraints.

We, now, establish the correctness of Algorithm <ref> using the following theorem:

Given sketch $\sketch$ and sample $\sample$,  Algorithm <ref> terminates and completes $\sketch$ to output an LTL formula that is consistent with $\sample$, if such a formula exists.

While Algorithm <ref> optimizes for the size of the inferred specification, it may not always return an minimal LTL formula.
Example <ref> demonstrates one such situation where Algorithm <ref> could produce a sub-optimal result.

Consider the sketch $\sketch=\placeholder_0 \lor \lnext\lnext p$ (Figure <ref>) and sample $\sample$ consisting of positive examples $\{\}\{p\}\{\}^\omega$ and $\{\}\{\}\{p\}\{\}^\omega$ and a negative example $\{\}^\omega$.
For this input, a possible output by Algorithm <ref> is the formula
$\leventually p\lor \lnext\lnext p$ (Figure <ref>).
The minimal consistent formula $\lnext p\lor \lnext\lnext p$ (Figure <ref>), however, is smaller.

(1) at (0, 0) $\lor$;
(2) at (-.5, -.7) $\placeholder^0$;
(3) at (0.5, -.7) $\lnext$;
(4) at (0.5, -1.4) $\lnext$;
(5) at (0.5, -2.1) $p$;
[->] (1) – (2);
[->] (1) – (3);
[->](3) – (4);
[->] (4) – (5);

[Possible formula]

(1) at (0, 0) $\lor$;
(2) at (-.5, -.7) $\leventually$;
(3) at (0.5, -.7) $\lnext$;
(4) at (0.5, -1.4) $\lnext$;
(5) at (0.5, -2.1) $p$;
(6) at (-0.5,-1.4) $p$;
[->] (1) – (2);
[->] (1) – (3);
[->] (3) – (4);
[->] (4) – (5);
[->] (2) – (6);

[Minimal formula]

(1) at (0, 0) $\lor$;
(2) at (0, -.7) $\lnext$;
(3) at (0, -1.4) $\lnext$;
(4) at (0, -2.1) $p$;
[->] (1) – (2);
[->] (1) edge [bend right] (3);
[->] (2) – (3);
[->] (3) – (4);

Minimal formulas require sharing of nodes

We leave the challenging problem of devising algorithms for searching for minimal LTL formulas from a given sketch as a part of future work.

§ EXPERIMENTAL EVALUATION

In this section, we design experiments to answer the following research question: how do the presented algorithms perform in terms of their running times and the size of inferred specification?
Can the algorithms recover the specification intended by the engineer?

To answer these questions, we perform a comparative study of our algorithms (presented in Section <ref>).
Note that, to the best of our knowledge, none of the existing tools can solve the  problem the newly generated sample from which they learn is not ensured to produce the minimal formula.in its full generality.
Thus, we restrict ourselves to comparisons of the presented algorithms.

red!90!black, mark=none,
green!50!black, mark=none,
blue!90!black, mark=none

group style=
group size=2 by 1,
ylabels at=edge left,

horizontal sep=1cm
xlabel=Number of benchmarks,
ylabel=Acc. time in $s$,
axis lines=left,
tick align=outside,
title style=font=, at=(axis description cs:0.5, .8), anchor=north, inner sep=0pt,

cycle list name=mylist,
axis on top,

[title=Type-0 set]
table [x expr=+1, y=Algo1SAT-type0, col sep=comma] csv/time-accumulated.csv;
table [x expr=+1, y=Algo1DT-type0, col sep=comma] csv/time-accumulated.csv;
table [x expr=+1, y=Algo2-type0, col sep=comma] csv/time-accumulated.csv;

[title=Type-1-2 set]
[red!80!black, mark=none] table [x expr=+1, y=Algo1SAT-type12, col sep=comma] csv/time-accumulated.csv;
[blue!80!black, mark=none] table [x expr=+1, y=Algo1DT-type12, col sep=comma] csv/time-accumulated.csv;
[blue!80!black, mark=none] table [x expr=+1, y=Algo2-type12, col sep=comma] csv/time-accumulated.csv;

<ref> Algo1-SAT 1.5em <ref> Algo1-DT 1.5em <ref> Algo2

Accumulated runtime  of the algorithms on the two benchmark sets

We have implemented a prototype of our algorithms in a tool called  which is publicly available[<https://github.com/rajarshi008/LTL-sketcher>].
While Algorithm <ref> can exploit any LTL learning algorithm, we have chosen the algorithms presented by Neider and Gavran [27] in their state-of-the-art LTL learning tool——one based on SAT solving and one on decision tree learning.
We refer to Algorithm 1 relying on the SAT-based algorithm as  and the one relying on decision tree learning as .
We refer to Algorithm 2 as .

For generating our benchmarks, we used the synthetic benchmark set presented by Neider and Gavran.
Their benchmark set consists of 1196 samples generated from 12 different LTL properties, which originate from a study by Dwyer et al. [11].
Based on these samples, we generated two benchmark sets, which we refer to as the  set and the  set.
Each benchmark in these two sets is simply a pair ($\sketch$, $\sample$) consisting of a sample and a sketch, which forms the input to our presented algorithms.

For generating a benchmark $(\sketch, \sample)$ in  set, we choose a sample $\sample$ generated from LTL formula $\varphi$ from the 1196 chosen samples; then construct a sketch $\sketch$ from $\varphi$ by substituting an aritrarily chosen subformula of size at least $\floor{\abs{\varphi}/2}$ by a Type-0 placeholder.
In this manner, we obtain 1196 pairs $(\sketch, \sample)$ for the  set.
We repeat the same process for the  set, except that we construct a sketch $\sketch$ from $\varphi$ by substituting one aritrarily chosen operator by a Type-1 placeholder, if unary, otherwise with a Type-2 placeholder.
Here again we generate 1196 pairs $(\sketch, \sample)$ for the  set.

All the experiments are conducted on a single core of a Debian machine with
Intel Xeon E7-8857 CPU (at 3 GHz) using up to 6 GB of RAM. The timeout
was set to be 1200 s for the run of each algorithm on each benchmark.

group style=
group size=3 by 1,
ylabels at=edge left,
yticklabels at=edge left,
horizontal sep=1.25cm
tick align=inside,
title style=font=, at=(axis description cs:0.5, .8), anchor=north, inner sep=0pt,
cycle list name=mylist,
axis on top,

[xlabel=Algo1-SAT, ylabel=Algo1-DT]
[gray] (rel axis cs:0, 0) – (rel axis cs: 1, 1);
only marks,
mark options=fill=gray,
visualization depends on = 2*Freq-log1 ,
scatter/@pre marker code/.style=/tikz/mark size=,
scatter/@post marker code/.style=] table [col sep=comma,x=Algo1SAT1,y=Algo1DT1,meta index=2] csv/sizes.csv;
every mark/.append style=solid, fill=gray;

[xlabel=Algo1-SAT, ylabel=Algo2, ylabel shift=-1mm]
[gray] (rel axis cs:0, 0) – (rel axis cs: 1, 1);
only marks,
mark options=fill=gray,
visualization depends on = 2*Freq-log2 ,
scatter/@pre marker code/.style=/tikz/mark size=,
scatter/@post marker code/.style=] table [col sep=comma,x=Algo1SAT2,y=Algo22,meta index=2] csv/sizes.csv;
every mark/.append style=solid, fill=gray;

[xlabel=Algo1-DT, ylabel=Algo2, ylabel shift=-1mm]
[gray] (rel axis cs:0, 0) – (rel axis cs: 1, 1);
only marks,
mark options=fill=gray,
visualization depends on = 2*Freq-log3 ,
scatter/@pre marker code/.style=/tikz/mark size=,
scatter/@post marker code/.style=] table [col sep=comma,x=Algo1DT3,y=Algo23,meta index=2] csv/sizes.csv;
every mark/.append style=solid, fill=gray;

Comparison of sizes of resulting LTL formula on  set.

§.§.§ Comparison of runtime

First, we compare the three algorithms based on their runtimes on the  and the  benchmark sets.
Figure <ref> presents the accumulated runtimes of the algorithms on the two benchmark sets.
From the figure, we observe that the runtimes of  and  is higher than that of  on the  set.
In fact,  and  experiences 957 and 881 time-outs, respectively, while,  only 289 time-outs.
The superior performance of  can be attributed to the fact that  and  perform LTL learning on a newly generated sample $\sample'$ (as discussed in Section <ref>) of size $\mathcal{O}({\abs{\sample}^2})$, which turns out to be an expensive procedure in most cases.

On the  set, however,  and  display better runtime performance.
This is because for substituting Type-1 or Type-2 placeholders only,  and  do not generate new samples.
Rather, they only solve $\existFormula$ using a SAT-solver.
, on the other hand, additionally performs at least one iteration of its incremental SAT solving procedure.
This observation presents a possible future optimization of  to adapt based on the type of placeholder present in the sketch.

§.§.§ Comparison of formula sizes

We now compare the three algorithms based on the size of the resulting LTL formulas on the  set.
Figure <ref> presents a pair-wise comparison of the three algorithms in terms of size.
We notice that  produces the smallest formulas among all the algorithms.
This is because,  iteratively searches for consistent formulas of increasing size.
While  and  also try to optimize the size, the newly generated sample from which they learn is not ensured to produce the minimal formula.

§.§.§ Comparison of formula recovery

Finally, we compare the three algorithms based on whether they were able to recover the intended formula. In our experimental setup, we consider the intended formula to be the one that was used to generate the input sample.
Table <ref> illustrates the percentage of runs in which the intended formula was recovered by the three algorithms on  and  benchmark sets.
On  benchmark set, both  and  almost never produced the intended formula, while  produced the original formula in several runs.
A possible explanation can be that  searches for simple completions first, finding the intended formula often.
For Algo1, however, the intermediate samples generated will not be optimized to obtain the intended formulas.
On  benchmark set, on the other hand, all the algorithms recover the intended formulas in most runs.
This is because, the intermediate samples do not play a role in this benchmark set and thus, all the algorithms have a similar performance.

0.1     97.4

0     97.4

54.9     97.9

Percentage of runs in which intended formula is recovered

Overall, we conclude that Algorithm <ref> performs better, in terms of runtime, size and recovery of specifications, even when Algorithm <ref> uses state-of-the-art LTL learning techniques.

§ CONCLUSION AND FUTURE WORK

We have introduced LTL sketching, a novel way of writing formal specifications in LTL.
The key idea is that a user can write a partial specification, i.e., a sketch, which is then completed based on given examples of desired and undesired system behavior.
We have shown that the sketching problem is in  and presented two SAT-based sketching algorithms.
Our experimental evaluation has shown that our algorithms can effectively complete sketches consisting of different types of missing information.

A natural direction for future work is to lift the idea of specification sketching to other specification languages, such as Signal Temporal Logic (STL) [26], the Property Specification Language (PSL) [12], or Computation Tree Logic (CTL) [8].
We also plan to investigate how specification sketching can be applied to visual specifications, including UML (high-level) message sequence charts [17].
Moreover, we intend to extend the notion of sketching beyond the use of examples to fill out placeholders (e.g., by allowing the engineer to constraint placeholders using simple logical formulas or regular expressions).

[1]
Arif, M.F., Larraz, D., Echeverria, M., Reynolds, A., Chowdhury, O., Tinelli,
C.: SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces.
In: FMCAD. pp. 93–103. IEEE (2020)

[2]
Bacherini, S., Fantechi, A., Tempestini, M., Zingoni, N.: A story about formal
methods adoption by a railway signaling manufacturer. In: FM. Lecture Notes
in Computer Science, vol. 4085, pp. 179–189. Springer (2006)

[3]
Badeau, F., Amelot, A.: Using B as a high level programming language in an
industrial project: Roissy VAL. In: ZB. Lecture Notes in Computer
Science, vol. 3455, pp. 334–354. Springer (2005)

[4]
Balyo, T., Heule, M.J.H., Järvisalo, M.: SAT competition 2016: Recent
developments. In: 31st AAAI Conference on Artificial Intelligence, AAAI
'17. pp. 5061–5063. AAAI Press (2017)

[5]
Bowen, J.P.: Gerard o'regan: Concise guide to formal methods: Theory,
fundamentals and industry applications. Formal Aspects Comput.
32(1),  147–148 (2020)

[6]
Camacho, A., Icarte, R.T., Klassen, T.Q., Valenzano, R.A., McIlraith, S.A.:
LTL and beyond: Formal languages for reward function specification in
reinforcement learning. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth
International Joint Conference on Artificial Intelligence, IJCAI 2019,
Macao, China, August 10-16, 2019. pp. 6065–6073. ijcai.org (2019).
10.24963/ijcai.2019/840, <https://doi.org/10.24963/ijcai.2019/840>

[7]
Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear
temporal logic. In: ICAPS. pp. 621–630. AAAI Press (2019)

[8]
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons
using branching-time temporal logic. In: Logics of Programs, Workshop,
Yorktown Heights, New York, USA, May 1981. Lecture Notes in Computer Science,
vol. 131, pp. 52–71. Springer (1981). 10.1007/BFb0025774

[9]
Cofer, D.D., Miller, S.P.: DO-333 certification case studies. In: NASA
Formal Methods. Lecture Notes in Computer Science, vol. 8430, pp. 1–15.
Springer (2014)

[10]
Courtois, P.J., Seidel, F., Gallardo, F., Bowell, M.: Licensing of safety
critical software for nuclear reactors. common position of international
nuclear regulators and authorised technical support organisations.  (12
2015). 10.13140/RG.2.1.2789.8968

[11]
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for
finite-state verification. In: FMSP. pp. 7–15. ACM (1998)

[12]
Eisner, C., Fisman, D.: A Practical Introduction to PSL. Series on Integrated
Circuits and Systems, Springer (2006). 10.1007/978-0-387-36123-9

[13]
Fecko, M.A., Uyar, M.Ü., Amer, P.D., Sethi, A.S., Dzik, T., Menell, R.,
McMahon, M.: A success story of formal description techniques: Estelle
specification and test generation for MIL-STD 188-220. Comput. Commun.
23(12),  1196–1213 (2000)

[14]
Fijalkow, N., Lagarde, G.: The complexity of learning linear temporal formulas
from examples. CoRR  abs/2102.00876 (2021)

[15]
Fix, L.: Fifteen years of formal property verification in intel. In: 25 Years
of Model Checking. Lecture Notes in Computer Science, vol. 5000, pp.
139–144. Springer (2008)

[16]
Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking
at scale: Automated air traffic control design space exploration. In: CAV
(2). Lecture Notes in Computer Science, vol. 9780, pp. 3–22. Springer

[17]
Harel, D., Thiagarajan, P.S.: Message sequence charts. In: UML for Real -
Design of Embedded Real-Time Systems, pp. 77–105. Kluwer (2003).

[18]
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Software Eng.
23(5),  279–295 (1997)

[19]
Holzmann, G.J.: The logic of bugs. In: SIGSOFT FSE. pp. 81–87. ACM

[20]
Kim, J., Muise, C., Shah, A., Agarwal, S., Shah, J.: Bayesian inference of
linear temporal logic specifications for contrastive explanations. In:
IJCAI. pp. 5591–5598. ijcai.org (2019)

[21]
Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P.,
Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch,
H., Winwood, S.: sel4: formal verification of an operating-system kernel.
Commun. ACM  53(6),  107–115 (2010)

[22]
Lemieux, C., Beschastnikh, I.: Investigating program behavior using the texada
LTL specifications miner. In: ASE. pp. 870–875. IEEE Computer Society

[23]
Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining
(T). In: ASE. pp. 81–92. IEEE Computer Society (2015)

[24]
Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In:
MEMOCODE. pp. 43–50. IEEE (2011)

[25]
Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using
FDR. Softw. Concepts Tools  17(3),  93–102 (1996)

[26]
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals.
In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant
Systems, Joint International Conferences on Formal Modelling and Analysis of
Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and
Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24,
2004, Proceedings. Lecture Notes in Computer Science, vol. 3253, pp.
152–166. Springer (2004). 10.1007/978-3-540-30206-3_12

[27]
Neider, D., Gavran, I.: Learning linear temporal properties. In: FMCAD. pp.
1–10. IEEE (2018)

[28]
Pakonen, A., Pang, C., Buzhinsky, I., Vyatkin, V.: User-friendly formal
specification languages - conclusions drawn from industrial experience on
model checking. In: ETFA. pp. 1–8. IEEE (2016)

[29]
Pnueli, A.: The temporal logic of programs. In: FOCS. pp. 46–57. IEEE
Computer Society (1977)

[30]
Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scalable anytime algorithms for
learning formulas in linear temporal logic. CoRR  abs/2110.06726

[31]
Riener, H.: Exact synthesis of LTL properties from traces. In: FDL.
pp. 1–6. IEEE (2019)

[32]
Roy, R., Fisman, D., Neider, D.: Learning interpretable models in the property
specification language. In: IJCAI. pp. 2213–2219. ijcai.org (2020)

[33]
Schlör, R., Josko, B., Werth, D.: Using a visual formalism for design
verification in industrial environments. In: Services and Visualization:
Towards User-Friendly Design. Lecture Notes in Computer Science, vol. 1385,
pp. 208–221. Springer (1998)

[34]
Shah, A., Kamath, P., Shah, J.A., Li, S.: Bayesian inference of temporal task
specifications from demonstrations. In: NeurIPS. pp. 3808–3817 (2018)

[35]
Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf.
15(5-6),  475–495 (2013)

[36]
Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming
by sketching for bit-streaming programs. In: PLDI. pp. 281–294. ACM

[37]
Verhulst, E., de Jong, G.G.: Opencomrtos: An ultra-small network centric
embedded RTOS designed using formal modeling. In: SDL Forum. Lecture
Notes in Computer Science, vol. 4745, pp. 258–271. Springer (2007)

[38]
Wasylkowski, A., Zeller, A.: Mining temporal specifications from object usage.
Autom. Softw. Eng.  18(3-4),  263–292 (2011)

§ A RESTRICTED VERSION OF THE LTL SKETCH EXISTENCE PROBLEM IS -COMPLETE

The exact complexity lower bound of the  problem is open and adds to the list of open problems in the area of LTL inference (see Section 6 of [14]).
However, here we show that for a restricted version of the  in which Type-0 placeholders can only be substituted with propositions, one has $\NP$-completeness.

For introducing the , we use a modified definition of substitutions, which we refer to as restricted susbtitutions.
Precisely, a restricted substitution $s$ maps the Type-0 placeholders to propositions, that is, $s(\placeholder)\in \prop$ if $\placeholder\in\placeholderset_0$.

We, now, state the restricted version of the  problem as follows:
Given a sketch $\sketch$ and a sample $\sample = (P,N)$, does there exist a complete restricted substitution $s$ for $\sketch$ such that $f_s(\sketch)$ is consistent with $\sample$?

is in $\NP$

Here we exploit the verifier-based definition of $\NP$ and show that: for every sketch $\sketch$ and sample $\sample$ if there exists a suitable complete restricted substitution, then there exists a complete restricted substitution that has “size” atmost $\poly(|\sample|,|\sketch|)$ and also is verifiable in time $\poly(|\sample|,|\sketch|)$.
The size of a substitution $s$  is
$\size{s} = \sum_{\placeholder\in\placeholderset^0} \size{s(\placeholder)}$.
Here, since, Type-0 placeholders can only be replaced with propositions the witness, a substitution $s$, is clearly of size $\poly(|\sample|,|\sketch|)$ and verifying whether it is consistent with $\sample$ also requires time $\poly(|\sample|,|\sketch|)$.

is -Hard

For proving -hardness, we reduce $\SAT$ to the problem .
Precisely, given a propositional formula $f$ in CNF, we construct a sample $\sample$ and a sketch $\sketch$ to reduce
an instance of $\SAT$ to an instance of .

Let us then first formalize $f$.
Let $\{x_1,\ldots,x_n\}$ and $\{C_1,\ldots C_m\}$ be the set of variables and clauses of $f$, respectively.
We visualize $f$ as an $m\times n$ matrix $I_f$ that stores which variable appears in which clause.
Precisely, $I_f(i,j) =	1 \text{ if } x_j \in C_i; I_f(i,j) = -1 \text{ if } \neg x_j \in C_i;I_f(i,j) = 0 \text{ otherwise }$.

Now, to construct the sample $\sample$, first we define the following:
$F_{i,j} = \{p\} \text{ if } I_f = 1; F_{i,j} = \{q\} \text{ if } I_f = -1; F_{i,j} = \{p,q\} \text{ if } I_f = 0$.
The sample $\sample$ consists of one positive word $w_p=\{p,q\}^n\emptyset^\omega$ and negative words $w_{n_i}= F_{i,1}F_{i,2}\cdots F_{i,n}\emptyset^\omega$ for each $i\in\{0,\cdots, m\}$.

The sketch we use is the following $\sketch = \placeholder_1 \wedge \lnext \placeholder_2\wedge\cdots \lnext^{i-1} \placeholder_i \cdots \wedge\lnext^{(n-1)} \placeholder_n$.

Now proving the following claim completes the reduction:

$f$ is satisfiable if and only if there exists is a complete restricted substitution $s$ such that $f_s(\sketch)$ consistent with $\sample$.

Let $f$ be satisfiable with a satisfying assignment $v$ which maps variables of $f$ to 0 or 1.
Based on $v$, we compute substitution $s$ as follows:

\begin{align*}
s(\placeholder_i) =
\begin{cases}
q \text{ if } v(x_i)=1\\
p \text{ if } v(x_i)=0
\end{cases}
\end{align*}

We now consider the formula $\varphi = s(\placeholder_1) \wedge \lnext s(\placeholder_2) \wedge \cdots \lnext^{i-1} s(\placeholder_i) \cdots\wedge \lnext^{n-1} s(\placeholder_n)$, obtained by applying $s$ to $\sketch$.
We show that $\varphi$ is indeed consistent with $\sample$.

First, observe that the positive word $w_p$ satisfies $\varphi$. This is because, $\varphi$ requires at least one of the propositions $p$ or $q$ to be true in the first $n$ positions, which is the case in $w_n$.

Second, we show that none of the negative words satisfy $\varphi$ using contradiction.
Towards contradiction, assume that $V(\varphi,w_{n_i})=1$ for a negative word $w_{n_i}$.
In the corresponding clause $C_i$, we know that if $x_j$ appears a positive literal, then $w_{n_i}[j] = \{p\}$ and thus, for $w_{n_i}$ to satisfy $\varphi$, $\placeholder_j$ in $\sketch$ must be substituted by proposition $p$.
This means that $v$ assigns $x_j$ to 0.
Consequently, $v$ assigns positive literals to 0 and similarly, it assigns negative literals to 1.
This results in clause $C_i$ to be false and thus, contradicts that $v$ is an satisfying assignment.

($\Leftarrow$) Let $s$ be a complete restricted substitutions such that $f_s(\sketch)$.
Now, clearly, $s(\placeholder)$ will be either $p$ or $q$, since otherwise $f_s(\sketch)$ will not satisfy positive word $w_p$.
Thus, based on $s$, we define the assignment $v$ as follows:

\begin{align*}
v(x_i) =
\begin{cases}
1 \text{ if } \placeholder_i=q\\
0 \text{ otherwise } \placeholder_i=p
\end{cases}
\end{align*}

We now show that $v$ satisfies $C_i$ for any $i\in\{1,\cdots,m\}$.
Suppose not, then $v(x_j) = 0$ if $x_i$ appears positively in $C_i$,
and $v(x_j) = 1$ if $x_j$ appears negatively in $C_i$.
This, by construction, implies that $s(\placeholder_j)=p$ if $w_{n_i}[j]=\{p\}$ and $s(\placeholder_j)=q$ if $w_{n_i}[j]=\{q\}$.
This means $w_{n_i}$ satisfies $f_s(\sketch)$ leading to a contradiction.