11institutetext: University of Colorado Boulder11email:
<EMAIL_ADDRESS>22institutetext: Indian Institute of
Technology Bombay, Mumbai, India22email:
<EMAIL_ADDRESS>
# Integrating Explanations in Learning LTL Specifications from Demonstrations

Ashutosh Gupta 22 John Komp 11 Abhay Singh Rajput 22 Krishna Shankaranarayanan
22 Ashutosh Trivedi 11 Namrita Varshney 22

###### Abstract

This paper investigates whether recent advances in Large Language Models
(LLMs) can assist in translating human explanations into a format that can
robustly support learning Linear Temporal Logic (LTL) from demonstrations.
Both LLMs and optimization-based methods can extract LTL specifications from
demonstrations; however, they have distinct limitations. LLMs can quickly
generate solutions and incorporate human explanations, but their lack of
consistency and reliability hampers their applicability in safety-critical
domains. On the other hand, optimization-based methods do provide formal
guarantees but cannot process natural language explanations and face
scalability challenges. We present a principled approach to combining LLMs and
optimization-based methods to faithfully translate human explanations and
demonstrations into LTL specifications. We have implemented a tool called
Janaka  based on our approach. Our experiments demonstrate the effectiveness
of combining explanations with demonstrations in learning LTL specifications
through several case studies.

###### Keywords:

LTL Specification Mining Large Language Models

##  1 Introduction

Linear Temporal Logic [6] (LTL) is a succinct, unambiguous, and expressive
formalism that captures the properties of the dynamic evolution of reactive
systems. LTL specifications are widely supported across various formal methods
infrastructure from model checking [20, 29] and synthesis [9], to
specification mining [30, 31] and reinforcement learning [43, 12, 25].
However, eliciting an LTL specification largely remains a manual effort,
demanding both substantial familiarity with the system and a deep
understanding of logic. Consequently, capturing complex requirements in LTL
remains time consuming and error prone [50]. For these reasons, automated
approaches for extracting LTL specifications from demonstrations are an active
area of research [30, 3, 16].

The existing approaches for extracting LTL specifications from demonstrations
reduce the problem to optimization-based search within a class of LTL formulas
using some quantitative semantics of LTL. A key challenge in learning LTL from
demonstrations is that the demonstrations are finite length traces, while LTL
is interpreted over $\omega$-traces. Consequently, there may be several
explanations for a given set of demonstrations. For instance, the following
demonstrations
$\langle\left\\{p\right\\},\left\\{p\right\\},\left\\{p\right\\}\rangle$ can
be explained as $\textsf{G}p$ (globally $p$), $\operatorname{\mathsf{F}}p$
(eventually $p$), or as $p\wedge\textsf{X}p\wedge\textsf{X}\textsf{X}p$ ($p$
for the first $3$ time steps). In deciding among competing hypotheses,
learning algorithms often use rule-of-thumb regularization such as Occam’s
razor [8, 19, 7] in identifying their output. We argue that elicitation of LTL
formulae from demonstrations can be greatly aided by integrating human
gestalt111The Gestalt principles [39, 49] refer to insights into how humans
recognize patterns, group objects, extend incomplete data, and explain complex
concepts based on principles such as continuity, proximity, similarity, and
common fate. For instance, a designer, when faced with a sequence
$\mathtt{qpqpqpqpppp}$, which might be succinctly explained as a sequence
ending with a $\mathtt{p}$, may interpret this sequence by applying the
principle of continuity to explain that the system eventually settles in
$\mathtt{p}$. in form of explanations. Moreover, the recent success of large
language models (LLMs) in understanding and generating natural languages [38,
47, 40] makes this approach timely and possible. We study the problem of
extracting LTL from demonstrations and explanations to improve the scalability
and relevance of the produced LTL formulas. We leverage LLMs to translate
explanations into a form that can be exploited to extract LTL from
demonstrations.

Traces Expla- nation Large language model training prompts  Template
generation Fitness Repair Synthesized Formula $\phi$
$\langle\varphi_{1},{\ldots},\varphi_{k}\rangle$$\stackrel{{\scriptstyle
LTL}}{{Candidates}}$$\langle\tau_{1},{\ldots},\tau_{n}\rangle$$\stackrel{{\scriptstyle
LTL}}{{Templates}}$ Figure 1: Our method for synthesizing LTL formulas from
traces uses the intuition of an LLM to find possible answers and we correct
them using our fitness-aware search.

While both LLMs and optimization-based approaches can be used to extract LTL
specifications, they have complementary strengths. While LLMs can integrate
both demonstrations and explanations, identify saliency using attention
mechanism [47], and return unique and novel hypotheses, they often suffer from
hallucinations [52], returning fictional and untrustworthy answers. On the
other hand, optimization-based approaches cannot utilize natural language
explanations and suffer from scalability challenges. To overcome these
challenges, we propose integrating both demonstrations and natural language
explanations in extracting LTL specifications.

Our Approach. We employ quantitative semantics for LTL formulas over finite
traces as a quantitative measure of a formula’s fitness within the set of
demonstrations. This fitness measure is used not only to assess the quality of
hypotheses generated by an LLM but also to improve the fitness of the
resulting formulas through formula repair. Our high-level approach is outlined
in Figure 1. We input demonstrations in the form of system traces involving a
set of atomic propositions, along with natural language explanations provided
by the designer. We assume that salient atomic propositions have already been
incorporated in the explanations. After presenting some general prompts
regarding LTL syntax, the LLM generates a set of candidate formulas, denoted
as $\langle\phi_{1},\ldots,\phi_{k}\rangle$. We evaluate their fitness using
our quantitative semantics, and if any of the formulas pass a specified
threshold, we accept the corresponding hypothesis. However, if none of the
generated formulas are deemed suitable, we extract LTL subformulas from this
family, which serve as templates $\langle\tau_{1}\ldots,\tau_{k}\rangle$.
These formulas are subsequently input into our fitness repair algorithm, in
conjunction with the demonstrations, to synthesize a formula that offers a
more satisfactory explanation of the provided demonstrations.

Figure 2: Learning LTL specifications from explanations and demonstrations.

####  1.0.1 Motivating example.

We present a sample use case of our approach through a simple example. Let’s
consider a scenario where a web designer is keen on formalizing the
requirements for an app. This formalization should be extracted from the
following set of session logs with semicolon as a separator:

$\mathtt{...!p,r,q,s;!p,r,q,s;p,!r,q,s;q,!r,!s,p;q,!r,!s,p;!p,s,!r,q;!p,r,q,!s;...}$

Here, the symbol $\mathtt{p}$ stands for a user logging in, $\mathtt{q}$ for a
user continuing to use the app, $\mathtt{r}$ for the expiration of the
session, and $\mathtt{s}$ for a user logging out. While from this limited
information, it is difficult to formalize the behavior, the designer can
provide the following description:

> _It is always the case that when a user logs in, they will remain logged in
> until they either log out or their session expires._

$\mathsf{ChatGPT4.0}$, with some minimal LTL syntax prompts, demonstrations,
and explanations, can produce the following explanation
$\textsf{F}(p\implies\operatorname{\mathsf{X}}(q\operatorname{\mathbin{\mathsf{U}}}(r\lor
s)))$.

It is clear to see that the description does not match the behaviour expressed
in the explanations. Moreover, the session logs do not match this
specification as well. On the other hand, it has correctly predicted the
saliency of $(r\lor s)$, $q\operatorname{\mathbin{\mathsf{U}}}(r\lor s)$ and
an implication of predicate $p$. Janaka  is able to create templates from this
formula and invoke constraint solvers to discover an LTL formula providing an
improved fitness. The following LTL formula was generated in the process
$\textsf{G}(p\implies\textsf{G}(q\operatorname{\mathbin{\mathsf{U}}}(r\lor
s)))$, that arguably and quantitatively provides a better fit both for the
natural language explanation and the set of demonstrations. This interaction,
along with the the ground truth LTL formula, is shown in Figure 2.

This approach has been implemented in a Python-based tool, Janaka , to
synthesize LTL formulae from demonstrations and explanations. The tool
utilizes $\mathsf{Gurobi}$ [2] for constraint solving and can be interfaced
with $\mathsf{ChatGPT4.0}$, $\mathsf{Claude}$, or $\mathsf{Bard}$. However,
for our experiments we report results using $\mathsf{ChatGPT4.0}$ by OpenAI
[38] as an LLM model. Unless explicitly stated, we use the term LLM to refer
to $\mathsf{ChatGPT4.0}$. We conducted experiments over 17 case studies,
providing both demonstrations and natural language explanations of the
underlying system. The goal of our experiments is to address the following
research questions: 1) Can LLMs be used for learning LTL from demonstrations?
2) Can human explanations increase the reliability of hypotheses generated by
LLMs? and 3) Can we extract useful LTL patterns from the outputs of LLMs to
construct LTL formulas more efficiently than learning LTL directly from
demonstrations?

Our experiments demonstrate the effectiveness of combining explanations with
demonstrations in learning LTL specifications. We applied the LLM and tool
combination on a representative set of formulas and experimental results
suggest that our approach produces better quality formulas for 12 cases than
solely using an LLM. We also show that using traces improves the responses of
LLM for 10 cases and in three cases the response remained the same.

##  2 Problem Definition

For a predicate $p$ we write $[p]=1$ if $p$ is true and $0$ otherwise. An
_alphabet_ $\Sigma$ is a non-empty, finite set of _symbols_. A _finite word_
$w$ over $\Sigma$ is a finite sequence $\langle a_{1}a_{2}...a_{n}\rangle$ of
symbols from $\Sigma$. The empty sequence is called the empty word, denoted
$\epsilon$. An $\omega$ word $w$ over $\Sigma$ is a function
$w:\mathbb{N}\to\Sigma$. The domain of $w$, denoted $\mathsf{dom}(w)$ is the
set of positions in $w$. The length of a finite (or infinite) word $w$ is
denoted $|w|$ and is equal to the size of its domain. For a word
$w=a_{0}a_{1}\ldots$, and two indices $i\leq j\leq|w|$, we write $w[i,j]$ to
denote the sub-word $a_{i}a_{i+1}\dots a_{j}$. and $w[i]$ for the suffix of
$w$ starting at index $i$. Abusing notation, we write a finite word
$w=a_{0}a_{1}\cdots a_{n}$ over $\Sigma$ as a partial function
$w:\mathbb{N}\to\Sigma$ where $w(i)=a_{i}$ for $i\leq n$ and $w(i)$ is
undefined for $i>n$. Let $\Sigma^{*}$ and $\Sigma^{\omega}$ be the set finite
and infinite words over $\Sigma$, respectively.

###  2.1 Qualitative Semantics for LTL

Let $\mathcal{P}$ be a set of propositional variables. LTL [6] is an extension
of propositional logic with temporal modalities.

Formulas in LTL over $\mathcal{P}$ are defined by the following grammar:

$\varphi::=\mathsf{true}~{}|~{}a\in\mathcal{P}~{}|~{}\varphi_{1}\vee\varphi_{2}~{}|~{}\neg\varphi~{}|~{}\textsf{X}~{}\varphi~{}|~{}\varphi\operatorname{\mathbin{\mathsf{U}}}\varphi$

Using the above basic operators, other Boolean connectives such as
$\varphi\wedge\psi=\neg(\neg\varphi\vee\neg\psi)$ and
$\varphi{\implies}\psi=\neg\varphi\vee\psi$, as well as temporal operators
(_finally_)
$\textsf{F}\varphi=\mathsf{true}\operatorname{\mathbin{\mathsf{U}}}\varphi$
and (_globally_) $\textsf{G}\varphi=\neg\textsf{F}\>\neg\varphi$ can be
derived as syntactic sugar.

Let $\Sigma=2^{\mathcal{P}}$. The semantics of LTL over the set of
propositions $\mathcal{P}$ is defined over words in $\Sigma^{\omega}$. The
notation $w\models\varphi$ denotes that the word $w$ satisfies the formula
$\varphi$, while $w\not\models\varphi$ denotes that it does not.

  * •

$w[i]\models\mathsf{true}$.

  * •

$w[i]\models a$ if and only if $a\in w(i)$.

  * •

$w[i]\models\neg\varphi$ if and only if $w[i]\not\models\varphi$.

  * •

$w[i]\models\varphi\vee\psi$ if and only if $w[i]\models\varphi$ or
$w[i]\models\psi$.

  * •

$w[i]\models\textsf{X}\varphi$ if and only if $i+1\leq|w|$ and
$w[i+1]\models\varphi$.

  * •

$w[i]\models\varphi\operatorname{\mathbin{\mathsf{U}}}\psi$ if and only if
there exists $j\geq i\in\mathsf{dom}{(w)}$ such that $w[j]\models\psi$ and for
all $i\leq k<j$, $w[k]\models\varphi$.

We say $w\models\varphi$ if $w[0]\models\varphi$. The language of an LTL
formula $\varphi$ is defined as $L(\varphi)=\\{w\in\Sigma^{\omega}\mid
w\models\varphi\\}$. We say that two LTL formulas are language equivalent if
they accept the same language.

LTL formulas $\textsf{F}\textsf{G}p$ (eventually forever $p$) and
$\textsf{G}\textsf{F}p$ (infinitely often $p$) are not $\omega$-language
equivalent, but they are finite-language equivalent [17] capturing the set of
finite words ending with a $p$.

###  2.2 Quantitative semantics for LTL

Given an LTL formula $\varphi$ and a finite trace, we design two valuation
functions $[\\![{\varphi,w}]\\!]$ that quantify the fitness of $\varphi$ in
explaining $w$. These valuation functions are based on two recently introduced
quantitative semantics: Robust Semantics [3] and Discounted Semantics [4]. We
support both semantics to cater to two different intuitions behind the
synthesis problem that needs to be solved. The robust semantics returns a
positive value when a trace satisfies a formula and a negative value
otherwise. Moreover, higher positive and negative values convey the degree to
which a perturbed trace satisfies the formula. The discounted semantics
returns a value in the range $[0,1]$, characterizing the discounted
satisfaction.

The complexity of an LTL formula can result from two aspects: the complexity
of the temporal structure ($\textsf{G}p$ is simpler than
$p\wedge\textsf{X}p\wedge\textsf{X}\textsf{X}p$ in explaining the sample
$\langle\left\\{p\right\\}\left\\{p\right\\}{\left\\{p\right\\}}\rangle$ and
the complexity of the nesting structure (the formula $p$ is simpler than
$p\wedge\neg q$ for explaining the sample $\langle\left\\{p\right\\}\rangle$.
We use the temporal discounting parameter $\alpha$ and nesting discount factor
$\beta$ in weighing this source of complexity. We modify the semantics of [3]
and [4] to integrate these parameters.

####  2.2.1 Robust Semantics .

Let $0{\leq}\alpha{\leq}1$ and $0{\leq}\beta{\leq}1$ be temporal and nesting
discount factors. In the robust semantics [3], given an LTL formula $\varphi$
and a finite word $w\in\Sigma^{*}$, a valuation function
$[\\![{\varphi,w}]\\!]$ is defined as follows.

  * •

$[\\![{a,w}]\\!]=2\cdot[a\in w(0)]-1$ and $[\\![{\neg
a,w}]\\!]=-1\cdot[\\![{a,w}]\\!]$

  * •

$[\\![{\varphi\land\psi,w}]\\!]=\begin{cases}\beta\cdot[\\![{\varphi,w}]\\!]\cdot[\\![{\psi,w}]\\!]&\text{if~{}}[\\![{\varphi,w}]\\!]\geq
0\land[\\![{\psi,w}]\\!]\geq 0,\\\ -1&otherwise\end{cases}$

  * •

$[\\![{\varphi\lor\psi,w}]\\!]=\beta\cdot\begin{cases}\mathrm{avg}([\\![{\varphi,w}]\\!],[\\![{\psi,w}]\\!])&\text{if~{}}[\\![{\varphi,w}]\\!]\geq
0\wedge[\\![{\psi,w}]\\!]\geq 0,\\\
\max([\\![{\varphi,w}]\\!],[\\![{\psi,w}]\\!])&\text{otherwise}\end{cases}$

  * •

$[\\![{G\varphi,w}]\\!]=\beta\cdot\begin{cases}\displaystyle\sum_{i=0}^{|w|}\alpha^{i}[\\![{\varphi,w[i]}]\\!]&\text{if
}[\\![{\neg\varphi,w[t]}]\\!]<0,\text{ for all $t\leq|w|$},\\\
-1&\text{otherwise}.\end{cases}$

  * •

$[\\![{F\varphi,w}]\\!]=\beta\cdot\begin{cases}\alpha^{t}[\\![{\varphi,w[t]}]\\!]&\text{where
}t=\min\\{j|[\\![{\varphi,w[j]}]\\!]\geq 0\\},\\\
\gamma\cdot\alpha^{|w|}&\text{if }[\\![{\varphi,w[t]}]\\!]=0~{}\text{for
all}~{}t.\end{cases}$

  * •

$[\\![{(X\varphi,w)}]\\!]=\begin{cases}[\\![{\varphi,w[1]}]\\!]&\text{if
}[\\![{\varphi,w[1]}]\\!]\geq 0\land|w|>1\\\ \gamma&\text{if~{}}|w|<2\\\
-1&\text{otherwise}.\end{cases}$

  * •

$[\\![{\varphi
U\psi,w}]\\!]=\begin{cases}\alpha^{t}\cdot[\\![{\psi,w[j]}]\\!]&t=\min\\{j|[\\![{\psi,w[j]}]\\!]\geq
0\\}\text{ and }[\\![{\varphi,w[i]}]\\!]\geq 0\text{ for all }i<t,{}\\\
\alpha^{|w|}\cdot\gamma&\text{if }[\\![{\psi,w[i]}]\\!]\geq 0\text{ for all
$i\leq|w|$}\\\ -1&\text{ otherwise}.\end{cases}$

######  Proposition 1 (Qualitative Equivalence: Robust)

If $\alpha=1$ then for every finite trace $w\in\Sigma^{*}$, we have that
$[\\![{\varphi,w}]\\!]=1$ if and only if $w\models\varphi$.

####  2.2.2 Discounted Semantics .

Let $0{\leq}\alpha{\leq}1$ and $0{\leq}\beta{\leq}1$ be temporal and nesting
discount factors. For a finite trace $w$ and LTL formula $\varphi$, we define
the valuation of $\varphi$ wrt $w$, $[\\![{\varphi,w}]\\!]$ as follows:

  * •

$[\\![{\mathsf{true},w}]\\!]=1$.

  * •

$[\\![{a,w}]\\!]=1$ if and only if $w(0)\ni a$.

  * •

$[\\![{\neg\varphi,w}]\\!]=1-[\\![{\varphi,w}]\\!]$.

  * •

$[\\![{\varphi\vee\psi,w}]\\!]=\beta\cdot\max\left\\{[\\![{\varphi,w}]\\!],[\\![{\psi,w}]\\!]\right\\}$.

  * •

$[\\![{\textsf{X}\varphi,w}]\\!]=\alpha[\\![{\varphi,w[1]}]\\!]$.

  * •

$[\\![{\varphi\operatorname{\mathbin{\mathsf{U}}}\psi,w}]\\!]=\max\limits_{0\leq
i<|w|}\left\\{\min\left\\{\alpha^{i}\cdot[\\![{\psi,w[i]}]\\!],\min\limits_{0\leq
j<i}\left\\{\alpha^{j}\cdot[\\![{\varphi,w[i]}]\\!]\right\\}\right\\}\right\\}.$

For G and $\operatorname{\mathsf{F}}$ operators, these semantics follow from
those of $\operatorname{\mathbin{\mathsf{U}}}$ and given here for
completeness:

  * •

$[\\![{\operatorname{\mathsf{F}}\varphi,w}]\\!]=\max\limits_{0\leq
i<|w|}\left\\{\alpha^{i}\cdot[\\![{\varphi,w[i]}]\\!]\right\\}.$

  * •

$[\\![{\textsf{G}\varphi,w}]\\!]=1-\max\limits_{0\leq
i<|w|}\left\\{\alpha^{i}\cdot[\\![{\neg\varphi,w[i]}]\\!]\right\\}=1-\max\limits_{0\leq
i<|w|}\left\\{\alpha^{i}\cdot(1-[\\![{\varphi,w[i]}]\\!])\right\\}.$

These quantitative semantics are similar to discounted semantics defined in
[4] except that our semantics introduce an additional discounting for Boolean
operators and they have been defined for finite traces.

######  Proposition 2 (Qualitative Equivalence: Discounted)

If $\alpha=1$ and $\beta=1$ then for every finite trace $w\in\Sigma^{*}$, we
have that $[\\![{\varphi,w}]\\!]=1$ if and only if $w\models\varphi$.

###  2.3 Mining LTL from Demonstrations and Explanations

A _sample_ , or set of demonstrations, $\mathcal{S}$ is a finite set of traces
$P\subseteq(2^{\mathcal{P}})^{*}$. In this work, depending on the context, we
use the term trace and demonstration interchangeably. For an LTL formula
$\varphi$, we say $\mathcal{S}\models\varphi$ iff for every $\tau\in P$ we
have that $\tau\models\varphi$. Given a sample $\mathcal{S}$, we are
interested in learning an LTL formula $\varphi$ such that
$\mathcal{S}\models\varphi$. While the qualitative criterion for fitness may
not be selective enough, as there may be multiple LTL hypotheses that satisfy
a given sample, we argue that instead of making decisions based on Occam’s
razor principles, it is arguably better to integrate designer’s insight in
selecting competing hypotheses. For this reason, we study the following
problem.

######  Definition 1 (Qualitative Mining for LTL)

Given a set of demonstrations $\mathcal{S}$, and a natural language
explanation $\mathcal{E}$ of the system capturing designer’s insights,
synthesize an LTL formula $\varphi$ such that $\mathcal{S}\models\varphi$.

Constraint solvers such as $\mathsf{Gurobi}$ can be used to synthesize LTL
formulas from demonstrations; however, they are unable to process natural
language explanations. LLMs, on the other hand, can work with both
explanations and demonstrations, but do not provide formal guarantees. We
posit that LLMs can often generate a set of competing hypotheses such that
while none of the proposed formulas may capture the specification in its
entirety, together they capture different salient features from the
explanation. To utilize this feature of LLMs, while providing formal
guarantees, we use constraint solvers to mix-and-match features from this set
of formulas to generate the final formula.

To measure the partial fitness of a formula over demonstrations and to aid in
combining the best-performing formulas, we use quantitative semantics defined
in the previous section as a fitness measure. For a given semantics
$[\\![{\cdot}]\\!]$, a sample $\mathcal{S}$, the valuation of $\varphi$ with
respect to $\mathcal{S}$ is defined as the average of all valuations over all
traces in the sample, i.e.,
$[\\![{\varphi,\mathcal{S}}]\\!]=(1/|w|)\cdot\sum_{w\in\mathcal{S}}[\\![{\varphi,w}]\\!]$.
We will refer to $[\\![{\varphi,\mathcal{S}}]\\!]$ and $[\\![{\varphi,w}]\\!]$
as the _fitness_ of $\varphi$ with respect to the sample $\mathcal{S}$ and
$w$, respectively. Our approach tackles a quantitative relaxation of the
previous problem.

######  Definition 2 (Quantitative Mining for LTL)

Given a set of demonstrations $\mathcal{S}$, and a natural language
explanation $\mathcal{E}$ of the system capturing designer’s insights, and a
bound $\kappa$, learn an LTL formula $\varphi$ such that
$[\\![{\varphi,\mathcal{S}}]\\!]\geq\kappa$.

##  3 Quantitative Mining for LTL

Our approach to generate and repair LTL from LLMs is shown in Algorithm 1. The
input to the LLM consists of a set $T$ of traces, a natural language
description of the formulas, and a fixed prompting text for LTL syntax. We
prompt the LLM to output a fixed number of formulae $\psi_{1},\dots,\psi_{N}$
(Algorithm 1, line 1), evaluate them based on the valuation function described
above, and if satisfactory (fitness beyond the tolerance) return the best fit
formula. Otherwise, we compute the top $k$ fit formulas (line 1) and generate
templates from these formulas using Algorithm 2 as follows. From the parse
tree of $\Psi_{top}$ ($Tree(\Psi_{top}$)) we synthesize a _template_ as shown
in Figure 3. A template is obtained by randomly choosing a node, say $v$, in
$Tree(\Psi_{top})$ and replacing it with a tree of height $\leq d$ for some
chosen $d\geq 1$ while preserving the following:

  1. 1.

If $v$ has only one child in $Tree(\Psi_{top})$, then the template hides the
label of node $v$ making it a hole which can be filled, and also adds a tree
$t^{\prime}$ as its right child. All nodes of $t^{\prime}$ are holes, which
need to be filled, and its height is $\leq d$.

  2. 2.

If $v$ has two children in $Tree(\Psi_{top})$, then the template only hides
the label of $v$ making it a hole to be filled.

  3. 3.

If $v$ is a leaf node in $Tree(\Psi_{top})$, then the template makes the label
of $v$ a hole and adds a tree $t^{\prime}$ of height $\leq d$ at $v$, with all
nodes of the newly added tree $t^{\prime}$ being holes to be filled.

Thus, we replace $v$ with a _template hole_ whose depth is $\leq d$. Note that
the choice of the node $v$ is non-deterministic (line 2 in Algorithm 2). Thus,
Algorithm 2 starts with $\Psi_{top}$, and a chosen $d\geq 1$, and outputs a
new parse tree containing template holes. The height of the new tree is $\leq
d+\textsf{height}(Tree(\Psi_{top})$. In line 1 of Algorithm 1, let
$\Psi_{temp}$ be the parse tree generated using Algorithm 2.

1

$\Psi\leftarrow$ API2LLM(T, E, P) ;

// API call to LLMs

2

3if  _$\max_{\psi\in\Psi}\\{[\\![{\psi,T}]\\!]\geq\kappa$_ then return
$\operatorname*{argmax}_{\psi\in\Psi}\\{[\\![{\psi,T}]\\!]\\}$;

4 else

$\Psi_{top}\leftarrow\displaystyle\mathrm{top\\_k}_{\psi\in\Psi}\\{[\\![{\psi,T}]\\!]$
} ;

// Returns top $k$ fit formulas

5

$\Psi_{temp}\leftarrow$ TemplateGen($\Psi_{top}$,d) ;

// Generate templates

6

return $\textsc{LTLRepair}(T,\Psi_{temp},d,\kappa)$ ;

// Repair LTL from templates

7

Algorithm 1 Janaka (Traces T, Explanations E, Prompt P, d, $\kappa$)

1

2Combine the given formulas $\Psi$ to construct a parse tree Tree($\Psi$);

3

4for  _each visit to a node of Tree( $\Psi$) in breadth-first order_ do

5 if  _$\textsc{random}(0,1) <0.2$_ then

6 Replace the node in Tree($\Psi$) by a template hole of depth $\leq d$

7return _Tree( $\Psi$)_;

8

Algorithm 2 TemplateGen(Set of LTL Formulas $\Psi$, Depth d)

Construct tree constraint $\Phi^{template}_{d}$ from $\Psi$ ;

// Constraints in eq.(2)-(11)

Construct trace constraint $\Phi^{T}_{d}$ ;

// Constraints in eq.(13)-(21)

1
$\mathtt{fitness},m\leftarrow\max\left(\displaystyle\sum_{\tau=1}^{|X|}y_{1,0}^{\tau}\>|\>\tau\in
T\right)$ such that $m\models\Phi^{template}_{d}\land\Phi^{T}_{d}$

2if  _$\mathtt{fitness}\geq\kappa$_ then return the formula constructed from m
;

3 else return False ;

4

Algorithm 3 LTLRepair( Traces $T$, Templates $\Psi$, Depth $d$, $\kappa$)

###  3.1 LTL Repair Algorithm

Next, we use Algorithm 3 which takes as input the modified parse tree with
template holes, $\Phi_{temp}$, to synthesize an optimal formula with the
highest score given $\Phi_{temp}$, the set of traces $T$ and the depth $d$
which was used in the generation of the template holes. The optimal formula is
obtained by computing and optimizing the scores of a class of formulas whose
depth is at most $d+\textrm{depth}(\Phi_{top})$, and is constrained to be well
formed and satisfied by traces $T$. This is done by building a constraint
system and finding an optimal solution for it. The constraint system
$\Phi=\Phi^{template}_{d}\wedge\bigwedge_{\tau\in T}\Phi^{\tau}_{d}$ is
obtained as a conjunction of the constraints obtained by encoding the template
($\Phi^{template}_{d}$) as well as the traces ($\bigwedge_{\tau\in
T}\Phi^{\tau}_{d}$). The first part encodes the structure of the _template_ ,
while the second part encodes the _functional_ constraints based on the on the
_score_ of each node enforced by the operators in the formula. The template
constraints are uniform across both the robust and discounted semantics, while
the functional constraints depend on the chosen semantics.

To encode the formula structure, we use a syntax tree with identifiers
$\mathcal{N}=\\{1,2,\ldots,n\\}$ for the set of nodes, where
$n=|\mathcal{N}|$. We assume herein that the root node is identified as $1$.
We have the child relations $L$ and $R$, such that $(i,j)\in L$ (or $R$) iff
the node $j$ is the left (right) child of node $i$. The only child of unary
operators is considered as a left child by assumption. For each node
$i\in\mathcal{N}$ and possible label
$\lambda\in\mathcal{O}\;\cup\;\mathcal{P}$, we introduce a Boolean variable
$x_{i,\lambda}$ indicating whether the node is labelled with an operator
($\mathcal{O}$) or variable ($\mathcal{P}$). We consider $x_{i,l}^{\tau}$ as a
Binary variable where $i\in\text{nodes}$ and $l\in\mathcal{P}\cup\mathcal{O}$
and $\tau$ is a trace. $\mathcal{O}$ and $\mathcal{P}$ are the sets of all
operations and propositions, respectively. Let $Br$ be a binary operation
($\land$, $\lor$, $U$, $\implies$), $Ur$ denote a unary operator ($G$,
$F$,$X$), and $Lf$ denote a leaf node labeled by a proposition $\mathcal{P}$).

G$p$

(1)

$\phi$$p$$\phi$

G$p$ (2) G$\phi$ $\vee$$p$$q$ (3) $\phi$$p$$q$

Figure 3: Template Generation Methods

Depth One tree Constraints. In the case of a tree whose depth is one, we have
only a leaf node labeled by the propositional variables. Exactly one
propositional variable must be decorating a leaf node; this is captured by

$\displaystyle\sum_{\begin{subarray}{c}op\in
Lf\end{subarray}}x^{\tau}_{i,op}=1$ (1)

Tree Constraint(depth “d” $>$ 1). In the case of trees with a depth of more
than one, the constraints are formed based on whether each non-leaf node is
decorated by a unary or a binary operator. The constraints are a case analysis
depending on the operator labeling the nodes.

For every non-leaf node $j$ of parent node $i$, i.e., $(i,j)\in L$ or
$(i,j)\in R$, we have the following constraints:

$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq 2^{d-1}-1\\\
(i,j)\in L\cup
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Br}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in\mathcal{O}\end{subarray}}x^{\tau}_{j,op_{j}}=1$
(2) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq
2^{d-1}-1\\\ (i,j)\in
L\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Ur}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in\mathcal{O}\end{subarray}}x^{\tau}_{j,op_{j}}=1$
(3) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq
2^{d-1}-1\\\ (i,j)\in
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Ur}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in\mathcal{O}\end{subarray}}x^{\tau}_{j,op_{j}}=0$
(4) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq
2^{d-1}-1\\\ (i,j)\in L\cup
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Lf}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in\mathcal{O}\end{subarray}}x^{\tau}_{j,op_{j}}=0$
(5) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq
2^{d-1}-1\\\ (i,j)\in L\cup
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\mathcal{O}\end{subarray}}x^{\tau}_{i,op_{i}}=0\implies\sum_{\begin{subarray}{c}op_{j}\in\mathcal{O}\end{subarray}}x^{\tau}_{j,op_{j}}=0$
(6)

For every leaf node $j$ of parent node $i$, i.e., $(i,j)\in L$ or $(i,j)\in
R$, we have the following constraints:

$\displaystyle\bigwedge\limits_{\begin{subarray}{c}2^{d-1}\leq j\leq
2^{d}-1\\\ (i,j)\in L\cup
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Br}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in
Lf\end{subarray}}x^{\tau}_{i,op_{j}}=1$ (7)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}2^{d-1}\leq j\leq
2^{d}-1\\\ (i,j)\in
L\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Ur}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in
Lf\end{subarray}}x^{\tau}_{j,op_{j}}=1$ (8)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}2^{d-1}\leq j\leq
2^{d}-1\\\ (i,j)\in
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Ur}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in
Lf\end{subarray}}x^{\tau}_{j,op_{j}}=0$ (9)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}2^{d-1}\leq j\leq
2^{d}-1\\\ (i,j)\in L\cup
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\text{Lf}\end{subarray}}x^{\tau}_{i,op_{i}}=1\implies\sum_{\begin{subarray}{c}op_{j}\in
Lf\end{subarray}}x^{\tau}_{j,op_{j}}=0$ (10)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}2^{d-1}\leq j\leq
2^{d}-1\\\ (i,j)\in L\cup
R\end{subarray}}\;\sum_{\begin{subarray}{c}op_{i}\in\mathcal{O}\end{subarray}}x^{\tau}_{i,op_{i}}=0\implies\sum_{\begin{subarray}{c}op_{j}\in\text{Lf}\end{subarray}}x^{\tau}_{j,op_{j}}=0$
(11)

####  3.1.1 Trace Constraints.

Next, we encode the functional constraints imposed by the operators for
discounted semantics. Trace constraints for the robust semantics are analogous
and given in Appendix 0.C. For this, to each node $i\in\mathcal{N}$, we attach
a set of real variables $Y^{\tau}_{i}=\\{y^{\tau}_{i,t}\;\mid 0\leq
t\leq|\tau|,i\in\mathcal{N}\\}$ representing its _score_ at each point $0\leq
t\leq|\tau|$ in a trace $\tau\in T$, where $y^{\tau}_{i,t}$ is defined below.
For a given trace $\tau$ we construct $\varphi^{\tau}_{0}pt$ as the
conjunction of:

$\displaystyle 0<y^{\tau}_{1,0}\leq 1$ (12)
$\displaystyle\bigwedge\limits_{1\leq i\leq
n}\bigwedge\limits_{p\in\mathcal{P}}\;\;x_{i,p}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\begin{cases}1&~{}if~{}p\in\tau(t)\\\
0&~{}if~{}p\not\in\tau(t)\end{cases}\right]$ (13)
$\displaystyle\bigwedge\limits_{1\leq i\leq
n}\bigwedge\limits_{p\in\mathcal{P}}\;\;x_{i,!p}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\begin{cases}0&~{}if~{}p\in\tau(t)\\\
1&~{}if~{}p\not\in\tau(t)\end{cases}\right]$ (14)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\ (i,j)\in
L,\\\ (i,j^{\prime})\in
R\end{subarray}}\;\;x_{i,\land}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\min\\{y^{\tau}_{j,t},y^{\tau}_{j^{\prime},t}\\}\right]$
(15) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L,\\\ (i,j^{\prime})\in
R\end{subarray}}\;\;x_{i,\lor}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\max\\{y^{\tau}_{j,t},y^{\tau}_{j^{\prime},t}\\}\right]$
(16) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L,\\\ (i,j^{\prime})\in
R\end{subarray}}\;\;x_{i,\implies}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\max\\{1-y^{\tau}_{j,t},y^{\tau}_{j^{\prime},t}\\}\right]$
(17) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L\end{subarray}}\;\;x_{i,G}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\\{1-\max\limits_{t\leq
t^{\prime}\leq|T|}\\{\alpha^{t^{\prime}-t}\cdot
1-y^{\tau}_{j,t^{\prime}}\\}\\}\right]$ (18)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\ (i,j)\in
L\end{subarray}}\;\;x_{i,F}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\max\limits_{t\leq
t^{\prime}\leq|T|}\\{\alpha^{t^{\prime}-t}\cdot
y^{\tau}_{j,t^{\prime}}\\}\right]$ (19)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\ (i,j)\in
L\end{subarray}}\;\;x_{i,X}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=y^{\tau}_{j,t+1}\right]$ (20)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq
n\end{subarray}}\;\;x_{i,U}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\min\left\\{\alpha^{i}\cdot[\\![{\psi,w[i]}]\\!],\min\limits_{0\leq
j<i}\left\\{\alpha^{j}\cdot[\\![{\varphi,w[i]}]\\!]\right\\}\right\\}\right]$
(21)

For each Boolean variables and operator, the constraints encode the valuation
of a node as a function of the valuation of its children.

The score for a node labelled G at a position $t$ in the trace is described by
the constraint (18). We encode the actual score as a function of its child,
adding the child’s score over all future positions in the input word, scaled
by an exponential. We also check that the G-property holds in a classical
sense, i.e., that its child has non-negative valuation at all positions.
Similarly, F is encoded in constraint (19), where we look for the first future
position $t^{\prime}$ where its child has non-negative valuation. The score of
its child is exponentially scaled so as to diminish the contribution from an
occurrence far away from the start. Finally, we optimize the score of the
template using the score of the root node $y^{\tau}_{1,0}$ w.r.t. the
constraint system $\Phi$ ( Algorithm 3). Then we use the resulting model to
fill the holes in the template, obtaining the optimal formula for the chosen
depth. By iterating over $0pt$, we may obtain the minimal such formula. Next,
we establish the correctness and soundness of this algorithm.

##  4 Experiments

We now present details of our implementation of Algorithm 1, including the
design of Janaka , evaluation benchmarks, experimental setup, and experimental
results. Our tool, Janaka  implements the algorithm in Python and employs
$\mathsf{Gurobi}$ [2] as a constraint solver. It exposes several configurable
hyperparameters to the designer, as shown in Figure 4, including the choice of
LLMs (OpenAI’s $\mathsf{ChatGPT4.0}$ [10], Anthropic’s $\mathsf{Claude}$ and,
Google’s $\mathsf{Bard}$), prompting strategy, templates, and semantics.

TracesTraceswith descriptionInput
TypeChatGPTBardClaudeLLMOneShotMultiShotPrompt$\psi$WithGFRandomG-TempTemplate
StrategyRobustDiscountedSemantics$F$ Figure 4: The high-level architecture of
Janaka .

###  4.1 LLM Setup

To inform the LLM regarding the syntax and semantics of our specifications and
demonstrations, we provide a fixed prompt to the LLM with each example (see,
Appendix 0.D). This prompt also includes the set of salient predicates present
in traces.

For each experiment, we also supply the LLM with the traces and explanation
(natural language description) of the desired formula and ask the LLM to
generate five LTL formulas such that each formula should satisfy all traces
and resemble the English description. We also conduct an ablation study, where
we repeat the test without the explanation. Janaka  verified each LLM
generated formula on the rules previously given; if any failed, we requested a
new formula. Due to cost limitations, we used the web interface to interact
with $\mathsf{ChatGPT4.0}$ and the other LLMs, thereby limiting the size and
quantity of our experiments. As an example of the limitations, the free
version of Claude has a strict rate limit restricted the number of experiments
that could be performed in a 24 hour period and a size limit on the input.

Table 1: Example LTL formulas with their natural language description and source. Index |  Original formula |  Input Description | Source
---|---|---|---
1 |  $G((p\Rightarrow F(q))\land(r\Rightarrow G(s)))$ |  In a financial monitoring system, it is always the case that when unusual account activity is detected (p), a fraud investigation is eventually initiated (q), and if regulatory compliance checks are required (r), continuous monitoring is implemented (s). For example, detecting suspicious transactions triggers a future fraud investigation, and if regulations are involved, ongoing compliance monitoring is maintained. | spot
2 |  $F(p\land(q\Rightarrow(r\land G(s))))$ |  At some point, the system will enter a critical state and if a user tries to access it, then the system will deny access and consistently send alerts. (system will enter a critical state=p, user tries to access = q, the system will deny access=r, send alerts=s) | spot
3 |  $G((a\lor b)\Rightarrow X((c)U(d\land F(e))))$ |  In a smart home security system, it is always the case that if either a window (a) or a door (b) is opened, then in the subsequent moment, the system continuously checks for motion detection (c) until it identifies a potential intruder (d) and eventually activates an alarm (e). | spot
4 |  $G((a\lor b)\Rightarrow X((c\land X(d))U(e)))$ |  In a complex manufacturing process, it is always the case that when either a raw material (a) or a semi-finished product (b) is processed, then in the next phase, the system ensures a specific manufacturing step (c) is completed and immediately followed by another step (d), continuously until the final inspection (e) is reached. | spot
5 |  $G(p\Rightarrow X((q)U(r\lor s)))$ |  It is always the case that when a user logs in, they will remain logged in until they either log out or their session expires. (p = user logs in, q = user remained logs in , r = session expires, s = logged out) | spot
Table 2: Janaka  Robust Semantics performance over LLM with description. We show the LLM ouput used for template generation. We present the formula with maximum manual score, the sum of their fitness over all the input traces (fit columns), and if the formula satisfies all traces. The times are in seconds. Formula |  LLM | SAT | FIT | Manual |  Janaka  | SAT | FIT | Manual | Runtime
---|---|---|---|---|---|---|---|---|---
1 |  $G(p\Rightarrow X(F(q)\land(r\Rightarrow X(G(s)))))$ | ✓ | 8.99 | 3.75 |  $G((p\Rightarrow G((F(q)\land(r\Rightarrow X(G(s)))))))$ | ✓ | 36.11 | 4.75 | 47.58
2 |  $F(p)\land(q\Rightarrow X(r\land F(s)))$ | × | 0.21 | 3.75 |  $(F(p)\land(q\Rightarrow X((r\Rightarrow F(s)))))$ | ✓ | 0.29 | 4.50 | 2889.43
3 |  $G((a\lor b)\Rightarrow X(G(c)U(d\land F(e))))$ | × | 1.72 | 3.75 |  $G(((a\lor b)\Rightarrow F((G(c)\lor(d\land F(e))))))$ | ✓ | 4.97 | 2.50 | 23.28
4 |  $G((a\lor b)\Rightarrow F(c\land(X(d)Ue)))$ | ✓ | 2.32 | 3.50 |  $G(((aUb)\Rightarrow F((c\land(X(d)Ue)))))$ | ✓ | 2.53 | 3.50 | 226.99
5 |  $F(p\Rightarrow X(qU(r\lor s)))$ | ✓ | 0.60 | 0.75 |  $G((p\Rightarrow G((qU(r\lor s)))))$ | ✓ | 8.79 | 4.25 | 64.37
Table 3: Janaka  Discounted Semantics performance over LLM with Description. For a detailed description of columns look at caption of Table 2 Formula |  LLM | SAT | FIT | Manual |  Janaka  | SAT | FIT | Manual | Runtime
---|---|---|---|---|---|---|---|---|---
1 |  $G(p\Rightarrow(F(q)\land(r\Rightarrow G(s))))$ | ✓ | 0.37 | 3.75 |  $G((p\Rightarrow(F(q)\land(s\lor G(\lnot r)))))$ | × | 0.59 | 3.00 | 129.85
2 |  $F(p\land q\Rightarrow X(r\land F(s)))$ | ✓ | 0.77 | 4.25 |  $F(((p\land q)\Rightarrow X((r\land F(s)))))$ | ✓ | 0.61 | 4.25 | 45.35
3 |  $G((a\lor b)\Rightarrow X(G(c)U(d\land F(e))))$ | × | 0.43 | 3.75 |  $G(((a\lor b)\Rightarrow F((G(c)\Rightarrow(d\land F(e))))))$ | ✓ | 0.54 | 5.00 | 125.89
4 |  $G(G((a\lor b)\Rightarrow X(c\land Xd))Ue)$ | × | 0.73 | 4.25 |  $G((G(((a\lor b)\Rightarrow X((c\land X(d)))))Ue))$ | × | 0.27 | 4.25 | 4.60
5 |  $GF(p\Rightarrow X(qU(r\lor s)))$ | ✓ | 0.57 | 1.00 |  $G(F((p\Rightarrow F((qU(r\lor s))))))$ | ✓ | 0.69 | 4.25 | 39.92
Table 4: Performance of LLM with and without traces. Formula |  LLM with traces | SAT | FIT | Manual |  LLM without traces | SAT | FIT | Manual
---|---|---|---|---|---|---|---|---
1 |  $G(p\Rightarrow X(F(q)\land(r\Rightarrow X(G(s)))))$ | ✓ | 8.99 | 3.75 |  $G(p\land r)\Rightarrow(F(q)\land(r\land(G(s))))$ | ✓ | 0.10 | 3
2 |  $F(p\land q\Rightarrow X(r\land F(s)))$ | ✓ | 0.77 | 4.25 |  $Fp\land G(q\Rightarrow X(r\land(G(s))))$ | × | 0.10 | 3.5
3 |  $G((a\lor b)\Rightarrow F((c)U(d\land F(e))))$ | × | 3.51 | 5 |  $G((a\lor b)\Rightarrow X(G(c)U(d\land X(e))))$ | × | -0.009 | 3.5
4 |  $G(G((a\lor b)\Rightarrow X(c\land Xd))Ue)$ | × | 0.27 | 4.25 |  $G((a\lor b)\Rightarrow X(c\land d)Ue)$ | × | 0.13 | 4.25
5 |  $G(p\Rightarrow(qU(r\lor s)))$ | ✓ | 4.36 | 3.00 |  $G(p\Rightarrow X(qU(s\lor(r\land\lnot q))))$ | ✓ | 0.53 | 1.75

###  4.2 Experimental Results

We synthesize templates from the LLM-produced formula with the best fitness
using three different strategies. In the first strategy, we implemented a
general randomization strategy, which involved modifying the tree structure by
selecting random nodes and replacing them with a tree of height $\leq d$ as
mentioned in Section 4. The second entailed the specific fixation of the
operators G and F in addition to the first. This adjustment was integrated as
a direct response to the LLM’s tendency to generate outputs that closely
correspond with the English descriptions but lacking the necessary temporal
operators. The third strategy focused on adding random quantifiers at the root
node, a measure to maintain the inherent structure of the formulas generated
by the LLM, and then synthesizing the template by the first strategy. Among
these three strategies, the second yielded the least effective results,
contributing minimally to enhancing formula fitness. Conversely, the third
strategy proved to be beneficial in elevating formula fitness. Additionally,
the randomization approach demonstrated superior performance. In our
experiments, we used mixed of the above strategies and repeatedly ran the tool
until it yielded formulas with high fitness.

Janaka  implements formula synthesis using both of our described semantics
using fitness-based encoding for both of the semantics to find the best
formula using $\mathsf{Gurobi}$. We add additional constraints to ensure that
$\mathsf{Gurobi}$ did not return a trivial formula by limiting its search
space, e.g., formulas like $p\lor\lnot p$ (tautology) or $FFp$ or equivalent
sub-formulas like $F(p)\land F(p)$ and various other optimization strategies
to reduce the search space. We ran $\mathsf{Gurobi}$ with a time limit and if
the time limit was hit, it returned the best solution found so far.

Table 1 shows a small selection of the seventeen formulas used in our
experiments as examples of the original formula and natural language
description. We originally looked at the formulas presented in [3], but the
LLM could solve them without any issues, which answers our first research
question 1 positively. To exercise our tool we required more complicated
formulas or a conjunction of many smaller formulas (such as our motivating
example).

Each of our experiment formulas required a set of traces and a natural
language description. To obtain such inputs, we started with an LTL formula
which was converted to a Büchi automaton using Spot[20], a platform for LTL
and $\omega$ -automaton manipulation. We non-deterministically walked the
resulting automaton to generate a set of traces that each ended in an
accepting states. The natural language description for the formula was written
manually creating a scenario that reflected the formula logic.

Tables 2 and 3 present results of our Robust Semantics and Discounted
Semantics experiments for the formulas in Table 1. In these tables, we show
the resulting best formula obtained by Janaka  after evaluations. Final
formula evaluation was done three ways: fitness score, satisfaction with input
traces, and manual grading. Manual grading on a scale of 1 to 5 was based on
the extracted formula’s expression of the original formula’s safety and
liveliness requirements along with how well it met the intent of the overall
specification. For each experiment we’ve recorded the run time of Janaka
alone because LLM response was typically short, benefiting from large cloud
computing resources, while the optimization query in Janaka  runs
significantly longer on a local PC.

In the end, 16 of the 17 the LLM generated and tool corrected formulas were
sufficient to express the intent of the original formulas. In the case of the
failing formula, the LLM was unable to generate any useful response.
Additionally, we found that Janaka  has improved the quality for 12 of the LLM
generated formula.

In our experiments, LLM produced formulas with better quality for 10 and the
same quality for 3 inputs when traces were provided.

Once we introduce the natural description of the original formula LLM
performance improved significantly, which answers our research question 2
positively.

We observe for most of the cases, an LLM can find formulas that are reasonably
close to the description and Janaka  can improve the quality of the resulting
formulas most of the time with good fitness and similarity to the original
formula as manually judged.

We found that both semantics produced interesting formulas though Discounted
Semantics had a higher incidence of producing formulas that are not satisfied
by all the traces.

###  4.3 Ablation Study

As an ablation study, we tested the impact of the natural language description
in the LLM’s performance by providing only traces for the formula generation
step of our process. We found that the LLMs struggled to produce any useful
formula. Due to this poor performance we did not include them in our
experimental results. We repeated the ablation testing by removing the traces
from the process to examine the impact of the descriptions alone. Table 4
contrasts the learned formulas and their scores for the cases when we provided
traces and when we did not. We observed that the LLM’s success was dependent
on several factors, the given detail of the original descriptions, their
degree of specificity, and the LLM’s ability to understand how the temporal
operators F and G define acceptance of future parts of the trace. Finally, to
test the contribution of the LLM and Janaka  to the overall results, Janaka
was given the formula traces and an empty template, testing if it could
generate the formulas from scratch. Within the given processing timeout, no
useful formulas were obtained. This result answers research question 3
positively.

We trained the LLM models in two modes: one-shot learning and multishot
learning. In one shot learning, we trained the LLM using examples and ground
rules to give the LLM an understanding of the LTL and the synthesis problem.
The chat is presented in Appendix 0.D. In multishot learning, we divide the
problem into sub-tasks and ask the LLM to generate a formula. Initially, we
provided the English description plus one trace. Subsequently, we increased
the subset size to three traces and then to six traces. After each increase in
traces, we ask the LLM to analyze and verify the given traces alongside the
English description. We observed the LLM give an average formula at the first
step, and with each addition of traces, it keeps adding small modifications to
the formula using LTL operators, which results in poor performance. We found
the first method more effective than the latter one. Our reported results are
using one-shot learning with $\mathsf{ChatGPT4.0}$.

##  5 Related Work

Grammatical inference [33] is concerned with learning formal languages as
grammars and their automata representations [26, 18]. Active techniques rely
on querying the system under learning to guide the inference process, whereas
passive grammatical inference leverages a static set of trace behavior without
making further queries for additional data. The former is exemplified by
$L^{\star}$ algorithm [5], whereas the latter generally relies on state-
merging procedures and can be used to learn probabilistic automata [13], MDPs
in the context of model checking [35], timed automata [34], and regular
decision processes [1].

The problem of learning LTL formulae from traces is a form of grammatical
inference that has been well-studied. Several of the methods most related to
our own are presented in [30, 37, 42, 48]. The focus of [37] is to produce the
minimal formula which is consistent with a rational sample represented as a
lasso. The problem of matching formulae with traces is encoded as a constraint
system and a satisfying assignment yields the learned property. However,
requiring the inputs to be lassos significantly restricts the application to
real scenarios. The method in [30] requires a user-defined input template of
the LTL formula which they would like to satisfy and outputs all possible
propositional substitutions consistent with the sample. Kim [28] select the
best candidate LTL templates that satisfy the given positive and negative
traces based on Bayesian probability.

Unlike these works, we use positive traces generated without restrictions for
our learning. While [23] has shown the difficulty of this approach, recent
work has focused on method to overcome the restriction. Roy [42] explored a
method that progressively builds a DFA from a trivial single satisfying state
to the smallest non-trivial DFA that still maintains satisfaction of the
provided traces. Another form of progressively building a to final formula was
explored in [48]. Their approach started with a known good formula and a set
of demonstrations that defined a new, related specification. Using a trellis
structure, they progressively update the formula, pruning the sections that do
not extend the formula in support of the additional specification. Our
approach works in a progressive manner but, unlike these approaches, we start
with candidate LLM generated LTL formulas that are expected to contain errors
and uses small templates of LTL syntax to improve the overall satisfaction of
formulas against positive traces.

Extracting formal requirements from natural language text has been a focus of
extensive research [11]. While there has been progress using unrestricted
natural language specifications [27, 21], many techniques require conformance
of the requirements language to specific ontologies [44], sentence structure
[51] or unique requirements languages [22, 14, 45]. Recently [32, 24, 41, 15],
large language models have been utilized to translate LTL from natural
language. Liu et al. [32] propose Lang2LTL, a modular system that leverages
pretrained LLMs to extract referring expressions, corresponding real-world
landmarks, and finally translate the command into an LTL task specification
for robotic motion planning. Hahn et al. [24] study generalization abilities
of LLMs when translating natural language into formal specifications with
complex semantics. They report that LLMs maintain their generalization
capabilities from pre-trained knowledge of natural language to generalize to
variable names and operator descriptions. However none of these approaches
study the application of LLMs in extracting LTL from demonstrations or
descriptions. Mavrogiannis [36] uses an LLM trained with task examples and
allowed instructions for translating cooking instructions from random internet
recipes into LTL formulas. Closer to our approach is that of Rahmani et al.
[41] where the authors combine LLMs to generate candidate formulas directly
from a task description and then use component-based synthesis to improve on
the results. In contrast, our work is focused on using an LLM not to generate
exact LTL formulas but synthesizing candidate ones from positive, finite
traces that could then be repaired to maximize the best qualities of both the
LLM and existing LTL synthesis tools.

## References

  * [1] E. Abadi and R. I. Brafman, “Learning and solving regular decision processes,” in _Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI_. ijcai.org, 2020, pp. 1948–1954. [Online]. Available: https://doi.org/10.24963/ijcai.2020/270
  * [2] T. Achterberg, “What’s new in gurobi 9.0,” _Webinar Talk url: https://www. gurobi. com/wp-content/uploads/2019/12/Gurobi-90-Overview-Webinar-Slides-1. pdf_ , 2019.
  * [3] M. Afzal, S. Gambhir, A. Gupta, S. Krishna, A. Trivedi, and A. Velasquez, “Ltl-based non-markovian inverse reinforcement learning,” in _Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2023, London, United Kingdom, 29 May 2023 - 2 June 2023_ , N. Agmon, B. An, A. Ricci, and W. Yeoh, Eds. ACM, 2023, pp. 2857–2859. [Online]. Available: https://dl.acm.org/doi/10.5555/3545946.3599102
  * [4] R. Alur, O. Bastani, K. Jothimurugan, M. Perez, F. Somenzi, and A. Trivedi, “Policy synthesis and reinforcement learning for discounted ltl,” _arXiv preprint arXiv:2305.17115_ , 2023.
  * [5] D. Angluin, “Learning regular sets from queries and counterexamples,” _Information and computation_ , vol. 75, no. 2, pp. 87–106, 1987.
  * [6] C. Baier and J.-P. Katoen, _Principles of model checking_. MIT press, 2008.
  * [7] H. Bensusan, “God doesn’t always shave with occam’s razor—learning when and how to prune,” in _Machine Learning: ECML-98: 10th European Conference on Machine Learning Chemnitz, Germany, April 21–23, 1998 Proceedings 10_. Springer, 1998, pp. 119–124.
  * [8] A. Blumer, A. Ehrenfeucht, D. Haussler, and M. K. Warmuth, “Occam’s razor,” _Information processing letters_ , vol. 24, no. 6, pp. 377–380, 1987.
  * [9] A. Bohy, V. Bruyère, E. Filiot, N. Jin, and J.-F. Raskin, “Acacia+, a tool for ltl synthesis,” in _Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings 24_. Springer, 2012, pp. 652–657.
  * [10] G. Brockman, V. Cheung, L. Pettersson, J. Schneider, J. Schulman, J. Tang, and W. Zaremba, “Openai gym,” 2016.
  * [11] A. Brunello, A. Montanari, and M. Reynolds, “Synthesis of ltl formulas from natural language texts: State of the art and research directions,” in _26th International symposium on temporal representation and reasoning (TIME 2019)_. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
  * [12] A. Camacho, R. T. Icarte, T. Q. Klassen, R. A. Valenzano, and S. A. McIlraith, “Ltl and beyond: Formal languages for reward function specification in reinforcement learning.” in _IJCAI_ , vol. 19, 2019, pp. 6065–6073.
  * [13] R. C. Carrasco and J. Oncina, “Learning stochastic regular grammars by means of a state merging method,” in _International Colloquium on Grammatical Inference_. Springer, 1994, pp. 139–152.
  * [14] G. Carvalho, F. Barros, A. Carvalho, A. Cavalcanti, A. Mota, and A. Sampaio, “Nat2test tool: From natural language requirements to test cases based on csp,” in _Software Engineering and Formal Methods: 13th International Conference, SEFM 2015, York, UK, September 7-11, 2015. Proceedings_. Springer, 2015, pp. 283–290.
  * [15] M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel, “nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,” _arXiv preprint arXiv:2303.04864_ , 2023.
  * [16] G. De Giacomo and M. Vardi, “Synthesis for ltl and ldl on finite traces,” in _Twenty-Fourth International Joint Conference on Artificial Intelligence_ , 2015.
  * [17] G. De Giacomo and M. Y. Vardi, “Linear temporal logic and linear dynamic logic on finite traces,” in _IJCAI’13 Proceedings of the Twenty-Third international joint conference on Artificial Intelligence_. Association for Computing Machinery, 2013, pp. 854–860.
  * [18] C. De la Higuera, _Grammatical inference: learning automata and grammars_. Cambridge University Press, 2010.
  * [19] P. Domingos, “The role of occam’s razor in knowledge discovery,” _Data mining and knowledge discovery_ , vol. 3, pp. 409–425, 1999.
  * [20] A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu, “Spot 2.0—a framework for ltl and-automata manipulation,” in _International Symposium on Automated Technology for Verification and Analysis_. Springer, 2016, pp. 122–129.
  * [21] S. Ghosh, D. Elenius, W. Li, P. Lincoln, N. Shankar, and W. Steiner, “Arsenal: automatic requirements specification extraction from natural language,” in _NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings 8_. Springer, 2016, pp. 41–46.
  * [22] D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann, “Generation of formal requirements from structured natural language,” in _Requirements Engineering: Foundation for Software Quality: 26th International Working Conference, REFSQ 2020, Pisa, Italy, March 24–27, 2020, Proceedings 26_. Springer, 2020, pp. 19–35.
  * [23] E. M. Gold, “Language identification in the limit,” _Information and control_ , vol. 10, no. 5, pp. 447–474, 1967.
  * [24] C. Hahn, F. Schmitt, J. J. Tillman, N. Metzger, J. Siber, and B. Finkbeiner, “Formal specifications from natural language,” _CoRR_ , vol. abs/2206.01962, 2022. [Online]. Available: https://doi.org/10.48550/arXiv.2206.01962
  * [25] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-regular objectives in model-free reinforcement learning,” in _International conference on tools and algorithms for the construction and analysis of systems_. Springer, 2019, pp. 395–412.
  * [26] J. J. Horning, “A study of grammatical inference.” Stanford University California, Department of Computer Science, Tech. Rep., 1969.
  * [27] M. Ilieva and O. Ormandjieva, “Automatic transition of natural language software requirements specification into formal presentation,” in _International Conference on Application of Natural Language to Information Systems_. Springer, 2005, pp. 392–397.
  * [28] J. Kim, C. Muise, A. J. Shah, S. Agarwal, and J. A. Shah, “Bayesian inference of linear temporal logic specifications for contrastive explanations.” International Joint Conferences on Artificial Intelligence, 2019.
  * [29] J. Křetínskỳ, T. Meggendorfer, and S. Sickert, “Owl: a library for-words, automata, and ltl,” in _International Symposium on Automated Technology for Verification and Analysis_. Springer, 2018, pp. 543–550.
  * [30] C. Lemieux, D. Park, and I. Beschastnikh, “General ltl specification mining (t),” in _2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 2015, pp. 81–92.
  * [31] W. Li, L. Dworkin, and S. A. Seshia, “Mining assumptions for synthesis,” in _Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011)_. IEEE, 2011, pp. 43–50.
  * [32] J. X. Liu, Z. Yang, I. Idrees, S. Liang, B. Schornstein, S. Tellex, and A. Shah, “Lang2ltl: Translating natural language commands to temporal robot task specification,” _arXiv preprint arXiv:2302.11649_ , 2023.
  * [33] M. Lopes, F. Melo, and L. Montesano, “Active learning for reward estimation in inverse reinforcement learning,” in _Joint European Conference on Machine Learning and Knowledge Discovery in Databases_. Springer, 2009, pp. 31–46.
  * [34] H. Mao, Y. Chen, M. Jaeger, T. D. Nielsen, K. G. Larsen, and B. Nielsen, “Learning deterministic probabilistic automata from a model checking perspective,” _Machine Learning_ , vol. 105, no. 2, pp. 255–299, 2016.
  * [35] ——, “Learning markov decision processes for model checking,” _Electronic Proceedings in Theoretical Computer Science_ , vol. 103, pp. 49–63, 2012.
  * [36] A. Mavrogiannis, C. Mavrogiannis, and Y. Aloimonos, “Cook2ltl: Translating cooking recipes to ltl formulae using large language models,” _arXiv preprint arXiv:2310.00163_ , 2023.
  * [37] D. Neider and I. Gavran, “Learning linear temporal properties,” in _2018 Formal Methods in Computer Aided Design (FMCAD)_ , 2018, pp. 1–10.
  * [38] R. OpenAI, “Gpt-4 technical report,” _arXiv_ , pp. 2303–08 774, 2023.
  * [39] S. E. Palmer, “Visual perception of objects,” _Handbook of psychology_ , pp. 177–211, 2003.
  * [40] A. Radford, K. Narasimhan, T. Salimans, I. Sutskever _et al._ , “Improving language understanding by generative pre-training,” 2018.
  * [41] K. Rahmani, M. Raza, S. Gulwani, V. Le, D. Morris, A. Radhakrishna, G. Soares, and A. Tiwari, “Multi-modal program inference: a marriage of pre-trained language models and component-based synthesis,” _Proceedings of the ACM on Programming Languages_ , vol. 5, no. OOPSLA, pp. 1–29, 2021.
  * [42] R. Roy, J.-R. Gaglione, N. Baharisangari, D. Neider, Z. Xu, and U. Topcu, “Learning interpretable temporal properties from positive examples only,” in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 37, no. 5, 2023, pp. 6507–6515.
  * [43] D. Sadigh, E. S. Kim, S. Coogan, S. S. Sastry, and S. A. Seshia, “A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications,” in _53rd IEEE Conference on Decision and Control_. IEEE, 2014, pp. 1091–1096.
  * [44] D. Sadoun, C. Dubois, Y. Ghamri-Doudane, and B. Grau, “From natural language requirements to formal specification using an ontology,” in _2013 IEEE 25th International Conference on Tools with Artificial Intelligence_. IEEE, 2013, pp. 755–760.
  * [45] T. Santos, G. Carvalho, and A. Sampaio, “Formal modelling of environment restrictions from natural-language requirements,” in _Formal Methods: Foundations and Applications: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26–30, 2018, Proceedings 21_. Springer, 2018, pp. 252–270.
  * [46] P. Tabuada and D. Neider, “Robust linear temporal logic,” _arXiv preprint arXiv:1510.08970_ , 2015.
  * [47] A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, L. u. Kaiser, and I. Polosukhin, “Attention is all you need,” in _Advances in Neural Information Processing Systems_ , I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, Eds., vol. 30. Curran Associates, Inc., 2017. [Online]. Available: https://proceedings.neurips.cc/paper_files/paper/2017/file/3f5ee243547dee91fbd053c1c4a845aa-Paper.pdf
  * [48] M. Vazquez-Chanlatte, S. Jha, A. Tiwari, M. K. Ho, and S. Seshia, “Learning task specifications from demonstrations,” _Advances in neural information processing systems_ , vol. 31, 2018.
  * [49] J. Wagemans, J. H. Elder, M. Kubovy, S. E. Palmer, M. A. Peterson, M. Singh, and R. Von der Heydt, “A century of gestalt psychology in visual perception: I. perceptual grouping and figure–ground organization.” _Psychological bulletin_ , vol. 138, no. 6, p. 1172, 2012.
  * [50] M. W. Whalen, A. Gacek, D. Cofer, A. Murugesan, M. P. Heimdahl, and S. Rayadurgam, “Your” what” is my” how”: Iteration and hierarchy in system design,” _IEEE software_ , vol. 30, no. 2, pp. 54–60, 2012.
  * [51] R. Yan, C.-H. Cheng, and Y. Chai, “Formal consistency checking over specifications in natural languages,” in _2015 Design, Automation & Test in Europe Conference & Exhibition (DATE)_. IEEE, 2015, pp. 1677–1682.
  * [52] Y. Zhang, Y. Li, L. Cui, D. Cai, L. Liu, T. Fu, X. Huang, E. Zhao, Y. Zhang, Y. Chen _et al._ , “Siren’s song in the ai ocean: A survey on hallucination in large language models,” _arXiv preprint arXiv:2309.01219_ , 2023.

##  Appendix 0.A Rationale behind Robustness Semantics

In the robust semantics [3], given an LTL formula $\varphi$ and a trace $T$, a
valuation function $[\\![{\varphi,T}]\\!]$ is defined as follows.

  * •

$[\\![{(p,T)}]\\!]=\begin{cases}1&\text{if }p\in T(0),\\\ -1&\text{if }p\notin
T(0).\end{cases}$

  * •

$[\\![{(\neg p,T)}]\\!]=\begin{cases}1&\text{if }p\notin T(0),\\\ -1&\text{if
}p\in T(0).\end{cases}$

  * •

$[\\![{(\varphi\land\psi,T)}]\\!]=\begin{cases}\beta\cdot[\\![{(\varphi,T)}]\\!]\cdot[\\![{(\psi,T)}]\\!]&\text{if~{}}[\\![{(\varphi,T)}]\\!]\geq
0\land[\\![{(\psi,T)}]\\!]\geq 0,\\\ -1&\text{otherwise.}\end{cases}$

  * •

$[\\![{(\varphi\lor\psi,T)}]\\!]=\beta\cdot\begin{cases}\frac{([\\![{(\varphi,T)}]\\!]+[\\![{(\psi,T)}]\\!])}{2}&\text{if~{}}[\\![{(\varphi,T)}]\\!]\geq
0\wedge[\\![{(\psi,T)}]\\!]\geq 0,\\\
\max([\\![{(\varphi,T)}]\\!],[\\![{(\psi,T)}]\\!])&\text{otherwise.}\end{cases}$

  * •

$[\\![{(G\varphi,T)}]\\!]=\beta\cdot\begin{cases}\displaystyle\sum_{i=0}^{|T|}\alpha^{i}[\\![{(\varphi,T(i))}]\\!]&\text{if
}[\\![{(\neg\varphi,T(t))}]\\!]<0\hskip 2.84544pt\forall t,\\\
-1&\text{otherwise}.\end{cases}$

  * •

$[\\![{(F\varphi,T)}]\\!]=\beta\cdot\begin{cases}\alpha^{t}[\\![{(\varphi,T(t))}]\\!]&\text{where
}t=\min\\{j|[\\![{(\varphi,T(j))}]\\!]\geq 0\\},\\\
\gamma*\alpha^{|T|}&\text{if }[\\![{(\varphi,T(t))}]\\!]=0~{}\text{for
all}~{}t.\end{cases}$

  * •

$[\\![{(X\varphi,T)}]\\!]=\begin{cases}[\\![{(\varphi,T(1))}]\\!]&\text{if
}[\\![{(\varphi,T(1))}]\\!]\geq 0\land|T|>1\\\ \gamma&\text{if~{}}|T|<2\\\
-1&\text{otherwise}.\end{cases}$

  * •

$[\\![{(\varphi
U\psi,T)}]\\!]=\begin{cases}\alpha^{t}\cdot[\\![{(\psi,T(j))}]\\!]&\text{where}~{}t=\min\\{j|[\\![{(\psi,T(j))}]\\!]\geq
0\\}\text{~{}and}{}\\\ &\forall i<t,~{}[\\![{(\varphi,T(i))}]\\!]\geq 0\\\
\alpha^{|T|}\cdot\gamma&\text{if }\forall i[\\![{(\psi,T(i))}]\\!]\geq 0\\\
-1&\text{ otherwise}.\end{cases}$

For the literals, we assign valuation -1 or 1 depending on whether the trace
satisfies it or not. We interpret conjunction by taking the product of the
valuation of the individual conjuncts. This implies that both subformulae must
do well on the trace. This is better than assigning
$[\\![{(\varphi{\land}\psi,T)}]\\!]$ as the minimum of
$[\\![{(\varphi,T)}]\\!]$ and $[\\![{(\psi,T)}]\\!]$ [46]. This valuation
ensures that both $\varphi$ and $\psi$ must score high for $\varphi\land\psi$
to score high. However, the $\min$ function is not sensitive to the formula
that has a higher value. Therefore, the learning algorithm becomes unguided
for one part of the formula. This suggests a modification to the valuation
function that takes both the subformulae into account symmetrically, without
flattening one of the subformulae. Our valuation function for the conjunction,
defined as their product $[\\![{(\varphi,T)}]\\!]\cdot[\\![{(\psi,T)}]\\!]$,
is based on this idea.

We interpret disjunction as an average over the disjuncts when the valuations
of individual disjuncts are $\geq 0$. Likewise, if one of the disjuncts is
$\geq 0$ and the other is $<0$, then we choose the maximum value. This implies
that a disjunction scores well if any of the two disjuncts does well on the
trace.

Our interpretation of $\textsf{G}\varphi$ computes the discounted sum of the
value of $\varphi$ at each position of the word. To give less weightage to a
literal appearing further down in the trace as opposed to earlier, we apply
the temporal discount of $0<\alpha<1$. Our interpretation of
$\textsf{F}\varphi$ computes the discounted score of $\varphi$ at the earliest
position where $\varphi$ has a non-negative score.

The discount value $\alpha$ is a parameter defined by the user to control the
temporal complexity. Consider the formula $\varphi=\textsf{F}q$ for
$p,q\in\mathcal{P}$ and the trace

$T=\\{p\\}\\{p,r\\}\\{p\\}\\{p,s\\}\\{p\\}\\{p\\}\\{p,q\\}(\\{r\\}\\{q\\})^{*}$

Then $q$ holds for the first time at $T(7)$. Thus, $V(q,T[7:|T|])=1$, making
$V(\varphi,T)=\alpha^{7}$. Our valuation assigns non-zero scores only for
satisfiable formulae.

##  Appendix 0.B Rationale for Discounted Semantics

Let $0{\leq}\alpha{\leq}1$ and $0{\leq}\beta{\leq}1$ be temporal and nesting
discount factors. For a finite trace $w$ and LTL formula $\varphi$, we define
the valuation of $\varphi$ wrt $w$, $[\\![{\varphi,w}]\\!]$ as follows:

  * •

$[\\![{\mathsf{true},w}]\\!]=1$.

  * •

$[\\![{a,w}]\\!]=1$ if and only if $w(0)\ni a$.

  * •

$[\\![{\neg\varphi,w}]\\!]=1-[\\![{\varphi,w}]\\!]$.

  * •

$[\\![{\varphi\vee\psi,w}]\\!]=\beta\cdot\max\left\\{[\\![{\varphi,w}]\\!],[\\![{\psi,w}]\\!]\right\\}$.

  * •

$[\\![{\textsf{X}\varphi,w}]\\!]=\alpha[\\![{\varphi,w[1]}]\\!]$.

  * •

$[\\![{\varphi\operatorname{\mathbin{\mathsf{U}}}\psi,w}]\\!]=\max\limits_{0\leq
i<|w|}\left\\{\min\left\\{\alpha^{i}\cdot[\\![{\psi,w[i]}]\\!],\min\limits_{0\leq
j<i}\left\\{\alpha^{j}\cdot[\\![{\varphi,w[i]}]\\!]\right\\}\right\\}\right\\}.$

For G and $\operatorname{\mathsf{F}}$ operators, these semantics follow from
those of $\operatorname{\mathbin{\mathsf{U}}}$ and given here for
completeness:

  * •

$[\\![{\operatorname{\mathsf{F}}\varphi,w}]\\!]=\max\limits_{0\leq
i<|w|}\left\\{\alpha^{i}\cdot[\\![{\varphi,w[i]}]\\!]\right\\}.$

  * •

$[\\![{\textsf{G}\varphi,w}]\\!]=1-\max\limits_{0\leq
i<|w|}\left\\{\alpha^{i}\cdot[\\![{\neg\varphi,w[i]}]\\!]\right\\}=1-\max\limits_{0\leq
i<|w|}\left\\{\alpha^{i}\cdot(1-[\\![{\varphi,w[i]}]\\!])\right\\}.$

For a trace $w=\langle\left\\{\neg p\right\\}\left\\{\neg
p\right\\}\cdots\left\\{\neg p\right\\}\left\\{p\right\\}\left\\{\neg
p\right\\}\left\\{\neg p\right\\}\rangle$,
$[\\![{\operatorname{\mathsf{F}}p,w}]\\!]$ evaluates to $\alpha^{n}$ where $n$
is the first index at which $p$ becomes true. Similarly, for a trace
$w=\langle\left\\{p\right\\}\left\\{p\right\\}\cdots\left\\{p\right\\}\left\\{\neg
p\right\\}\left\\{p\right\\}\left\\{p\right\\}\rangle$,
$[\\![{\textsf{G}p,w}]\\!]$ evaluates to $1-\alpha^{n}$ where $n$ is the first
index in which $p$ becomes false. In summary,
$[\\![{\operatorname{\mathsf{F}}p,w}]\\!]$ is higher when $p$ is found
earlier, capturing the quantitative semantics for “eventually”. On the other
hand, $[\\![{\textsf{G}p,w}]\\!]$ is higher for a longer contiguous initial
sequence that the trace exhibits, capturing the quantitative semantics of
“globally.”

##  Appendix 0.C Trace Constraints for the Robust Semantics

To encode the formula structure according to the robust semantics, we use a
syntax tree with identifiers $\mathcal{N}=\\{1,2,\ldots,n\\}$ for the set of
nodes, where $n=|\mathcal{N}|$. We assume herein that the root node is
identified as $1$. We have the child relations $L$ and $R$, such that
$(i,j)\in L$ (or $R$) iff the node $j$ is the left (right) child of node $i$.
The only child of unary operators is considered as a left child by assumption.
For each node $i\in\mathcal{N}$ and possible label
$\lambda\in\mathcal{O}\;\cup\;\mathcal{P}$, we introduce a Boolean variable
$x_{i,\lambda}$ indicating whether the node is labelled with an operator
($\mathcal{O}$) or variable ($\mathcal{P}$).

Trace Constraints for the Robust semantics: We describe the functional
constraints imposed by the operators. For this, to each node
$i\in\mathcal{N}$, we attach a set of real variables
$Y^{\tau}_{i}=\\{y^{\tau}_{i,t}\;\mid 0\leq t\leq|\tau|,i\in\mathcal{N}\\}$
representing its _score_ at each point $0\leq t\leq|\tau|$ in a trace $\tau\in
T$, where $y^{\tau}_{i,t}$ is defined below. For a given trace $\tau$ and for
Robust Semantics we construct $\varphi^{\tau}_{0}pt$ as the conjunction of:

$\displaystyle y^{\tau}_{1,0}>=1$ (22) $\displaystyle\bigwedge\limits_{1\leq
i\leq
n}\bigwedge\limits_{p\in\mathcal{P}}\;\;x_{i,p}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\begin{cases}1&~{}if~{}p\in\tau(t)\\\
-1&~{}if~{}p\not\in\tau(t)\end{cases}\right]$ (23)
$\displaystyle\bigwedge\limits_{1\leq i\leq
n}\bigwedge\limits_{p\in\mathcal{P}}\;\;x_{i,!p}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\begin{cases}-1&~{}if~{}p\in\tau(t)\\\
1&~{}if~{}p\not\in\tau(t)\end{cases}\right]$ (24)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\ (i,j)\in
L,\\\ (i,j^{\prime})\in
R\end{subarray}}\;\;x_{i,\land}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\begin{cases}\beta\cdot y^{\tau}_{j,t}\cdot
y^{\tau}_{j^{\prime},t}&~{}if~{}y^{\tau}_{j,t}\geq 0\land
y^{\tau}_{j^{\prime},t}\geq 0\\\ -1&\textnormal{otherwise}\end{cases}\right]$
(25) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L,\\\ (i,j^{\prime})\in
R\end{subarray}}\;\;x_{i,\lor}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\begin{cases}\frac{y^{\tau}_{j,t}+y^{\tau}_{j^{\prime},t}}{2}&y^{\tau}_{j,t}\geq
0\land y^{\tau}_{j^{\prime},t}\geq 0\\\
\max\limits\\{y^{\tau}_{j,t},y^{\tau}_{j^{\prime},t}\\}&otherwise\end{cases}\right]$
(26) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L,\\\ (i,j^{\prime})\in
R\end{subarray}}\;\;x_{i,\implies}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\begin{cases}\frac{-y^{\tau}_{j,t}+y^{\tau}_{j^{\prime},t}}{2}&y^{\tau}_{j,t}<0\land
y^{\tau}_{j^{\prime},t}\geq 0\\\
\max\limits\\{-y^{\tau}_{j,t},y^{\tau}_{j^{\prime},t}\\}&otherwise\end{cases}\right]$
(27) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L\end{subarray}}\;\;x_{i,G}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\begin{cases}\sum^{|T|}_{t^{\prime}=t}\alpha^{t^{\prime}}\cdot
y^{\tau}_{j,t^{\prime}},&where~{}\forall
t^{\prime},y^{\tau}_{j,t^{\prime}}\geq 0\\\ -1&otherwise\end{cases}\right]$
(28) $\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\
(i,j)\in L\end{subarray}}\;\;x_{i,F}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\begin{cases}\alpha^{t^{\prime}}y^{\tau}_{j,t^{\prime}},&\textnormal{where
}t\leq t^{\prime}<|T|,t^{\prime}=\min\\{i\geq t|y^{\tau}_{j,i}\geq 0\\}\\\
\gamma\cdot\alpha^{|\tau|}&otherwise\end{cases}\right]$ (29)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq n,\\\ (i,j)\in
L\end{subarray}}\;\;x_{i,X}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\begin{cases}y^{\tau}_{j,t+1},&\textnormal{where,
}y^{\tau}_{j,t+1}\geq 0\\\ \gamma&~{}if~{}t+1\geq|\tau|\\\
-1&otherwise\end{cases}\right]$ (30)
$\displaystyle\bigwedge\limits_{\begin{subarray}{c}1\leq i\leq
n\end{subarray}}\;\;x_{i,U}\Rightarrow\left[\bigwedge\limits_{1\leq
t\leq|T|}y^{\tau}_{i,t}=\beta\cdot\begin{cases}\alpha^{t^{\prime\prime}}\cdot
y^{\tau}_{j,t^{\prime\prime}}&~{}if~{}\forall t^{\prime},t\leq
t^{\prime}<t^{\prime\prime},y^{\tau}_{j,t^{\prime}}\geq 0\land
y^{\tau}_{j,t^{\prime\prime}}\geq 0\\\
\gamma\cdot\alpha^{|\tau|}&~{}if~{}\forall iy^{\tau}_{j,t^{\prime}}\geq 0\\\
-1&\textnormal{ otherwise}\end{cases}\right]$ (31)

Corresponding to Boolean variables and to each operator, the constraints
encode the calculation of the valuation of a given node as a function of the
valuation of its children, as defined in Section 2.2.

##  Appendix 0.D Information about LLM (ChatGPT) Prompts

ChatGPT chat defining the rules the LLM must use for formula generation:

Training: This prompt aims to generate LTL formulas by observing a pattern in
given traces and taking hints from English description. English description is
like a hint that gives us an overview of what is happening in traces. ChatGPT:
Sure! For those unfamiliar, LTL stands for ”Linear Temporal Logic”. It’s a
type of logic used to describe properties of sequences of states in time. LTL
formulas are commonly used in the domain of formal verification, especially
for describing and checking the behaviors of systems over time. To generate an
LTL formula based on provided traces and English descriptions, I’ll need: 1\.
The traces, which are sequences of states or events that you’ve observed. 2\.
The English description that serves as a hint. Once you provide both, I’ll do
my best to capture the observed behavior as an LTL formula. Please go ahead
and provide the required details.

Training: These are the definitions of LTL terms: 1. $\pi\models\top$ 2.
$\pi\not\models\bot$ 3. $\pi\models p$ iff $p\in L(s_{1})$ 4.
$\pi\models\neg\phi$ iff $\pi\not\models\phi$ 5.
$\pi\models\phi_{1}\land\phi_{2}$ iff $\pi\models\phi_{1}$ and
$\pi\models\phi_{2}$ 6. $\pi\models\phi_{1}\lor\phi_{2}$ iff
$\pi\models\phi_{1}$ or $\pi\models\phi_{2}$ 7.
$\pi\models\phi_{1}\rightarrow\phi_{2}$ iff $\pi\models\phi_{2}$ whenever
$\pi\models\phi_{1}$ 8. $\pi\models X\phi$ iff $\pi_{2}\models\phi$ 9.
$\pi\models G\phi$ iff, for all $i\geq 1$, $\pi\models\phi$ 10. $\pi\models
F\phi$ iff there is some $i\geq 1$ such that $\pi_{i}\models\phi$ 11.
$\pi\models\phi U\psi$ iff there is some $i\geq 1$ such that
$\pi_{i}\models\psi$ and for all $j=1,\ldots,i-1$, we have
$\pi_{j}\models\phi$ $\phi$ is any formula:
$\phi::=\bot\,|\,p\,|\,(\neg\phi)\,|\,(\phi\land\phi)\,|\,(\phi\lor\phi)\,|\,(\phi\rightarrow\phi)\,|\,(X\phi)\,|\,(F\phi)\,|\,(G\phi)\,|\,(\phi
U\phi)$ ChatGPT: Understood. This is a basic definition of LTL semantics.
You’ve presented the meaning of various LTL operators in terms of how they
relate to traces (denoted as $\pi$). To make the task clear: You will provide
some traces (sequences of states/events). You will provide an English
description hinting at the behavior captured in those traces. Based on the
traces and the English description, I’ll generate an LTL formula capturing the
observed behavior. Please provide the traces and the English description so
that I can generate the LTL formula.

Training: Rules to follow for generating formulas: Note - 1. The formula
should include all variables present in traces. 2. If there are ’1’s at the
end of any trace, that means there is no pattern in traces. There is no
pattern. So, there cannot be ’G’ in the beginning of the formula. 3. If you
see terms like globally, for all, always, every time, and other similar terms,
use ’G’. 4. If you see terms like future, at some point, eventually, and other
similar terms, try to use ’F’. 5. If terms like until, till, and similar terms
are used, then try to use ’U’. Steps to follow when generating formulas: 1.
Follow all the above-mentioned rules carefully. 2. First, observe and find
patterns in traces without even looking at the English description. 3.
Generate 5 LTL formulas using pattern, observation, and English description,
such that each formula should satisfy all traces and resemble the English
description. 4. After generating formulas, verify that they follow all the
rules; otherwise, regenerate them. ChatGPT: Understood. I’ll follow these
steps and rules when generating the LTL formula. Please provide the traces and
the English description, and I’ll proceed to generate the LTL formulas based
on your specifications.

LLM Formula Extraction Examples

Training: Example 1 - Go through each step Input Traces where ”,” is the label
separator, ”;” is the state separator, and ”#” is the end of the trace:
p,!q,!r;!p,!q,!r;!p,!q,!r;p,q,!r;1;1;1;1;1;1#
p,q,r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
!p,!q,!r;p,q,!r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
p,!q,!r;!p,!q,!r;p,q,!r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;
1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
p,q,r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
p,q,!r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
!p,q,r;p,q,r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
p,q,r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
p,!q,!r;p,q,r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
p,q,!r;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1#
1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1;1# English Description: ”At some point during its operation, the software will experience a critical error (p) and will either generate an error report (q) or initiate a self-repair process (r).” ChatGPT: Let’s break down the task step by step, as per your instructions: 1\. Observe and find patterns in traces: Looking at the traces, some consistent patterns that emerge: \- There are traces with the sequence: !p,!q,!r; followed by p,q,!r; and then a series of 1; states. \- There are traces with the sequence: p,q,r; followed by a series of 1; states. \- Some traces have only 1; states. From this, we can deduce a few patterns: \- The critical error p happens either alone or with other events q or r. \- After the occurrence of p, the sequence tends to end or goes into a series of 1; states. 2\. Generate 5-LTL formulas: Given the English Description, we are looking for the occurrence of p and then either q or r. Considering the provided information and patterns observed: \- F(p & (q | r)) This formula ensures that at some point, there’s a state where p occurs and either q or r happens as well. \- F(p & q) | F(p & r) This formula breaks down the occurrences into two separate futures, one where p & q happens and another where p & r happens. \- F(p) -> X(q | r) This formula captures the essence that after p happens, in the next state either q or r will happen. \- F(p) & (F(q) | F(r)) This formula ensures that p will happen at some point and also either q or r will happen at some point. This is a bit weaker than the other formulas. \- G((p & !q & !r) -> X(q | r)) This formula globally ensures that whenever there’s a state where p happens and q and r don’t, in the next state either q or r should happen. 3\. Verification: All the above formulas follow the given rules: \- They include all the variables present in traces: p, q, r. \- They do not use G in the beginning as there are series of 1; states in the traces, indicating no global pattern. \- They align with the given English description. \- The most relevant formula, as you pointed out, is F(p & (q | r)). This formula aptly captures the essence of the English description.

Training: Example 2 - Go through each step Input Traces where “,” is the label
separator, “;” is the state separator, and “#” is the end of trace:
!p,q,r,s;!p,q,r,s;!p,!q,!r,!s;p,!q,!r,!s;p,!q,!r,!s;p,!q,r,!s;p,!q,!r,!s;
!p,q,!r,s;1;1#
!p,q,!r,!s;!p,!q,r,!s;p,q,r,s;!p,q,r,s;1;1;1;1;1;1#
!p,q,r,s;p,q,r,!s;!p,q,r,!s;1;1;1;1;1;1;1#
!p,q,r,s;p,q,!r,!s;!p,q,!r,s;1;1;1;1;1;1;1#
p,q,r,!s;!p,q,!r,!s;p,q,!r,!s;p,q,!r,!s;p,q,r,s;1;1;1;1;1#
!p,q,r,!s;p,q,!r,s;p,q,!r,s;1;1;1;1;1;1;1#
p,!q,r,s;p,q,r,s;1;1;1;1;1;1;1;1#
p,!q,r,!s;p,q,!r,s;1;1;1;1;1;1;1;1#
p,q,r,s;p,q,r,!s;1;1;1;1;1;1;1;1#
!p,!q,!r,s;!p,!q,!r,s;p,!q,r,!s;p,q,r,s;1;1;1;1;1;1# English Description: At
some point, the software will be updated (p), and in the next time period, the
system will verify its integrity (q) and either restart (r) or notify the user
of success (s). Most relevant formula: $F(p\&X(q\&(r|s)))$ ChatGPT: Let’s
follow the steps: 1\. Observe and find patterns in traces: Observing the
traces, we can identify a few patterns: \- After p occurs (i.e., the software
is updated), we see that q often follows in the next state, indicating
verification of integrity. \- Once q occurs, we observe that either r or s can
happen, representing the system restart or user notification, respectively.
2\. Generate 5-LTL formula: Given the English Description, after the
occurrence of p, in the next state q should occur, and then either r or s
should happen. From this understanding, we can form the following LTL
formulas: \- $F(p\&X(q\&(r|s)))$
This formula ensures that at some future point when the software is updated
(p), in the very next time frame, it will verify its integrity (q), and then
either restart (r) or notify the user (s). \- $F(p\&X(q))\&F(q\rightarrow
X(r|s))$
This formula breaks down the behavior into two separate future events. First,
the software gets updated and verifies its integrity. And when integrity is
verified, in the next state, the system either restarts or notifies the user.
\- $G(p\rightarrow X(q\&(r|s)))$
This formula ensures that globally, whenever the software updates, in the next
state it verifies its integrity and either restarts or notifies the user. \-
$F(p)\&F(q\&(r|s))$
This formula is a bit more relaxed. It ensures that at some point in the
future, the software will update, and at another point (not necessarily
immediately after), it will verify integrity and take action (either restart
or notify). \- $G(p\rightarrow X(q))\&G(q\rightarrow X(r|s))$
This formula breaks down the two-step behavior. It ensures that globally, when
the software updates, it will verify its integrity in the next state. Also,
once integrity is verified, in the next state, the system either restarts or
notifies the user. 3\. Verification: All the above formulas follow the given
rules: \- They include all the variables present in traces: p, q, r, s. \-
They do not start with G because of the series of 1; states in the traces,
indicating no global pattern. \- They align with the provided English
description. \- The most apt formula, as you mentioned, is
$F(p\&X(q\&(r|s)))$. This formula accurately captures the described behavior.

Training: Example 3 - Go through each step Input Traces where “,” is the label
separator, “;” is the state separator, and “#” is the end of trace:
!p,q,r,s;p,q,r,s;!p,!q,!r,s;!p,!q,r,s;p,q,r,!s;p,q,r,s;p,!q,!r,s;
!p,!q,!r,!s;!p,q,!r,!s;!p,q,r,!s#
p,!q,r,!s;!p,q,r,s;p,q,r,s;p,!q,r,s;!p,!q,r,s;p,q,r,!s;!p,!q,!r,s;
!p,q,r,s;!p,!q,r,!s;p,q,r,s#
p,q,r,!s;!p,!q,!r,s;p,!q,!r,!s;!p,!q,r,!s;p,!q,!r,s;!p,!q,r,!s;
p,q,r,s;!p,!q,r,s;!p,q,!r,!s;!p,!q,!r,!s#
!p,!q,r,!s;p,!q,r,s;p,!q,r,!s;!p,!q,r,!s;p,q,r,!s;p,q,r,s;p,q,r,s;
!p,!q,r,s;p,q,r,!s;p,q,r,s#
p,!q,r,s;!p,!q,!r,s;p,q,r,s;!p,!q,r,s;!p,!q,r,s;!p,!q,!r,!s;!p,q,!r,s;
!p,!q,!r,s;p,!q,!r,s;p,!q,r,!s#
p,!q,r,!s;p,q,r,s;p,q,r,s;!p,!q,r,s;!p,!q,r,s;p,!q,r,!s;p,!q,!r,s;
!p,q,!r,s;p,!q,!r,s;p,!q,r,!s#
!p,!q,r,s;p,q,r,s;p,!q,r,s;!p,!q,r,s;p,q,r,s;!p,!q,!r,s;!p,q,!r,!s;
!p,q,r,s;!p,!q,r,!s;!p,q,!r,s#
p,!q,r,s;!p,!q,r,s;p,q,r,!s;p,q,r,s;!p,!q,r,s;!p,q,r,!s;p,!q,!r,!s;
p,!q,!r,!s;p,!q,!r,s;p,q,r,s# English Description: Always, when the room is
occupied (p) and the lights are off (q), the motion sensors will activate (r),
and in the next time period, the emergency lights will turn on (s). Most
relevant formula: $G((p\land q)\to(r\land X(s)))$

ChatGPT: Let’s analyze the given traces based on the steps: 1\. Observe and
find patterns in traces: From the traces, we can observe: \- The sequence
p,q,!r,!s appears several times, indicating that sometimes the room is
occupied, the lights are off, but the motion sensors are not activated, and
the emergency lights don’t turn on. \- The sequence p,q,r,s appears several
times, indicating that sometimes when the room is occupied and the lights are
off, the motion sensors are activated, and the emergency lights are turned on
immediately. 2\. Generate 5-LTL formula: Given the English Description, always
when the room is occupied (p) and the lights are off (q), the motion sensors
will activate (r), and in the next time period, the emergency lights will turn
on (s). We can generate the following LTL formulas: \- $G((p\land q)\to(r\land
X(s)))$
This formula, which you identified as the most relevant one, captures the
behavior that globally, whenever the room is occupied and the lights are off,
the motion sensors will activate, and in the next time frame, the emergency
lights will turn on. \- $G(p\land q\to X(r\land s))$
This formula suggests that whenever the room is occupied and the lights are
off, in the next state, the motion sensors will activate, and the emergency
lights will turn on. \- $G(p\land q\to r)\&G(r\to X(s))$
This formula breaks down the behavior into two separate conditions. Globally,
when the room is occupied and the lights are off, the motion sensors activate.
Once motion sensors are activated, the emergency lights will turn on in the
next state. \- $G(p\land q\to X(r))\&G(r\to X(s))$
Here, it states that globally, when the room is occupied and lights are off,
in the next state, the motion sensors activate. And when motion sensors are
activated, in the next state, emergency lights will turn on. \-
$G(p\to(q\to(r\land X(s))))$
This formula suggests a cascading behavior, i.e., globally, whenever the room
is occupied, and then the lights are off, the motion sensors will activate,
and the emergency lights will turn on in the next time frame. 3\.
Verification: The provided traces and the English description align with the
following LTL formula: $G((p\land q)\to(r\land X(s)))$. This formula ensures
that always, whenever the room is occupied (p) and the lights are off (q), the
motion sensors will be activated (r), and in the subsequent time frame, the
emergency lights will turn on (s).

Training: Example 5 - Go through each step Input Traces where “,” is the label
separator, “;” is the state separator, and “#” is the end of trace:
!p,!q,r,s,t,u;p,!q,!r,s,!t,!u;!p,q,r,s,!t,u;1;1;1;1;1;1;1#
!p,!q,r,s,t,!u;p,!q,r,s,!t,u;1;1;1;1;1;1;1;1#
!p,q,r,s,!t,u;p,q,r,s,t,!u;p,q,r,s,!t,u;p,q,r,s,!t,!u;p,q,r,!s,!t,!u;
!p,q,r,s,t,u;!p,!q,r,s,t,!u;p,!q,r,s,t,!u;!p,!q,r,!s,t,u;p,!q,r,s,t,!u#
!p,!q,r,s,!t,!u;!p,!q,!r,!s,!t,u;1;1;1;1;1;1;1;1#
!p,q,r,!s,t,u;!p,q,r,s,!t,u;!p,!q,r,!s,!t,!u;p,q,r,s,!t,!u;p,q,r,!s,t,u;
!p,!q,r,!s,!t,!u;!p,!q,r,s,!t,!u;p,q,r,!s,t,!u;p,!q,r,s,!t,!u;p,q,r,s,t,u#
p,!q,r,s,!t,!u;!p,q,!r,s,!t,u;!p,!q,r,s,t,u;1;1;1;1;1;1;1#
p,q,!r,s,t,u;!p,q,!r,s,t,!u;1;1;1;1;1;1;1;1#
p,!q,!r,!s,t,!u;!p,q,r,!s,t,u;!p,!q,r,s,!t,!u;p,q,r,!s,t,u;!p,q,r,!s,!t,!u;
p,!q,r,s,t,u;!p,!q,r,!s,!t,!u;p,q,r,s,t,u;p,!q,r,s,t,!u;
p,q,r,!s,t,!u;p,q,r,s,!t,u#
p,q,r,s,!t,!u;!p,q,r,!s,t,!u;!p,q,r,s,t,u;p,!q,r,s,!t,!u;!p,q,r,s,t,!u;
p,q,r,s,!t,u;p,!q,r,s,!t,!u;p,q,r,!s,t,!u;p,q,r,s,!t,!u;p,q,r,s,t,u#
p,q,r,!s,t,u;!p,q,!r,s,t,u;p,!q,r,!s,t,u;1;1;1;1;1;1;1# English Description:
Either the system is in standby (p) or it’s active (q) and always from then on
processes tasks (r). This continues until it encounters an error (s) and in
the next time period either sends an alert (t) or eventually restarts (u).
Most relevant formula: $(p|(q\&G(r)))U(s\&X(t|F(u)))$

ChatGPT: Alright, let’s break down this problem step-by-step: 1\. Observe and
find patterns in traces: From the traces, we can identify: \- Sequences where
the system is active q and is consistently processing tasks r until it
encounters an error s. \- Sequences where upon encountering an error s, in the
next time period, an alert is sent t or eventually, the system restarts u. \-
Sequences where the system is on standby p. 2\. Generate 5-LTL formula: Given
the English Description: Either the system is in standby (p) or it’s active
(q) and always from then on processes tasks (r). This continues until an error
is encountered (s) and in the next time period either sends an alert (t) or
eventually restarts (u). We can generate the following LTL formulas: \-
$(p|(q\&G(r)))U(s\&X(t|F(u)))$: This formula captures the entire behavior
succinctly. It states that the system is either on standby or when it’s
active, it will keep processing tasks. This goes on until an error is
encountered. Upon encountering an error, in the next state, it will send an
alert or at some point, the system restarts. \- $(p|G(q\&r))U(s\&X(t|F(u)))$:
This formula says that the system is either on standby, or it is continuously
active and processing tasks until an error occurs. When the error occurs, it
will send an alert in the next state or eventually restart. \- $(p|G(q\to
r))U(s\to(X(t)|F(u)))$: This formula suggests that the system is either on
standby or when active, it processes tasks. When it encounters an error, it
will either send an alert in the next state or at some point in the future,
restart. \- $(p|G(q\&r))\&G(s\to(X(t)|F(u)))$: Breaking the formula into two
global conditions. One handles the behavior of the system being on standby or
active and processing tasks, and the other handles the behavior after
encountering an error. \- $(p|G(q\&r))\&(s\to X(t|u))$: This formula suggests
that if the system is on standby or is active and processing tasks, and if an
error is encountered, in the next state, it will either send an alert or
restart. 3\. Verification: Based on the traces provided and the English
description, the most fitting formula seems to be:
$(p|(q\&G(r)))U(s\&X(t|F(u)))$. This formula encapsulates the entire behavior.
The system is either on standby or when active, always processes tasks. This
behavior continues until an error is encountered, after which in the next
state, an alert is sent or at some point, the system restarts.

Training: Example 6 - Go through each step Input Traces where “,” is the label
separator, “;” is the state separator, and “#” is the end of trace:
p,!q,r;!p,q,r;!p,!q,!r;!p,q,!r;p,!q,r;!p,q,!r;p,q,r;!p,q,!r;p,!q,!r;!p,q,!r;
!p,!q,!r;!p,q,!r;p,!q,r;!p,q,r;p,!q,r;p,q,!r;!p,!q,!r;!p,q,r;!p,q,r;p,q,!r#
!p,q,!r;!p,q,!r;!p,q,!r;p,!q,!r;p,q,!r;p,!q,r;p,!q,!r;p,!q,!r;!p,q,r;
!p,q,r;p,!q,r;p,!q,!r;p,!q,!r;p,!q,r;!p,q,r;
!p,!q,!r;p,!q,r;p,!q,r;p,!q,!r;p,!q,!r;p,q,r#
p,!q,r;p,!q,!r;!p,q,!r;p,q,r;p,!q,r;!p,q,r;p,!q,!r;p,!q,r;p,!q,!r;!p,q,!r;
p,q,!r;!p,q,!r;!p,!q,!r;p,!q,r;p,!q,!r;p,!q,r;p,!q,r;p,!q,!r;p,!q,!r;p,q,r#
!p,q,!r;!p,!q,!r;p,!q,r;!p,q,r;!p,q,!r;!p,q,!r;p,!q,r;p,q,r;p,q,!r;p,q,r;
!p,q,r;!p,!q,!r;p,!q,r;p,!q,r;!p,q,r;p,!q,r;p,!q,r;p,q,r;p,q,!r;
p,q,!r;p,!q,r;!p,q,r;p,!q,r;!p,q,!r;p,!q,r;!p,q,!r;p,!q,r;p,!q,r;
p,!q,r;p,q,r#
p,!q,r;!p,q,r;p,!q,r;p,!q,r;!p,q,!r;p,!q,r;p,!q,r;p,q,r;p,q,!r;!p,!q,!r;
!p,q,!r;p,!q,r;!p,q,r;p,!q,!r;p,!q,r;p,!q,r;p,q,r;
p,!q,r;!p,q,!r;!p,q,r;p,!q,r;p,q,r;p,!q,r;p,q,!r;!p,q,!r;
p,!q,r;p,q,r;p,q,!r#
!p,q,!r;p,!q,!r;!p,q,!r;p,q,!r;!p,!q,!r;p,!q,r;p,!q,r;p,!q,r;p,!q,!r;!p,q,r;
p,q,!r;!p,q,!r;p,!q,!r;p,q,r;p,!q,r;p,!q,r;p,q,r;!p,q,!r;!p,q,r;p,!q,r;
p,!q,!r;p,!q,r;!p,q,r;p,q,!r;!p,q,!r;!p,q,r;p,q,r;p,q,!r;!p,q,r;p,q,!r;
!p,q,!r;p,q,r;p,q,!r#
p,!q,!r;p,!q,!r;!p,q,!r;p,!q,!r;!p,!q,!r;!p,q,r;!p,q,!r;p,!q,r;!p,q,!r;
!p,!q,!r;!p,!q,!r;p,!q,!r;p,!q,r;p,!q,r;!p,q,!r;p,!q,r;p,!q,r;p,!q,r;
p,!q,!r;p,q,r# English Description: ”Whenever a request is submitted (r), it
will continuously be in the processing state (p) until it is eventually
accepted (q).” Most relevant formula: $G(r\to(pUq))$

ChatGPT: Alright, let’s process the information given: 1\. Observe and find
patterns in traces: From the traces, we can make out the following: \- There
are sequences where after a request is submitted (r), it is in the processing
state (p) for a while and eventually gets accepted (q). \- There are sequences
where a request is submitted but it does not go into the processing state or
get accepted. 2\. Generate 5-LTL formula: Given the English Description:
”Whenever a request is submitted (r), it will continuously be in the
processing state (p) until it is eventually accepted (q).” We can generate the
following LTL formulas: \- $G(r\to(pUq))$: This is a straightforward
representation of the description. Whenever a request is submitted, it remains
in the processing state until it gets accepted. \- $G(r\to X(pUq))$: This
formula is slightly different from the first. It says that when a request is
submitted, in the next state, it will enter the processing state and
eventually get accepted. \- $G(r\&F(p)\&F(q))$: This formula suggests that
whenever a request is made, it will eventually be processed and accepted but
not necessarily in direct succession. \- $G(r\to(G(p)\;|\;F(q)))$: This
formula states that once a request is made, it will either be continuously
processed or will eventually be accepted. \- $G((r\&p)\to F(q))$: This formula
means that if a request is made and it’s in the processing state, it will
eventually be accepted. 3\. Verification: To verify the most fitting formula,
we will refer to the traces. From a preliminary look, many traces seem to fit
the pattern of once a request (r) is made, it stays in the processing state
(p) until it gets accepted (q). The most fitting formula that describes the
English description as well as adheres to the traces provided is:
$G(r\to(pUq))$. This formula captures the behavior that whenever a request is
submitted, it remains in the processing state until it gets accepted, which is
in line with the given English description and the provided traces.