<figure><img src="image_1.png" /></figure>

HAL
open science

# Formalizing Embedded Systems Requirements in Stereotyped Natural Language:

Gaétan Hains, Ouarda Fenek

► To cite this version:

Gaétan Hains, Ouarda Fenek. Formalizing Embedded Systems Requirements in Stereotyped Natural Language: 2024. hal-04754373

HAL Id: hal-04754373

https://hal.science/hal-04754373v1

Preprint submitted on 25 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
# Formalizing Embedded Systems Requirements in Stereotyped Natural Language: Deep Learning as a Certainly Approximately Correct Translation Automorphism *

Gaétan Hains¹* and Ouarda Fenek²

¹*LACL, Université Paris-Est Créteil, Créteil, 94000, France.

²R&D, Intellig'IA, Paris, 75000, France.

*Corresponding author(s). E-mail(s): gaetan.hains@u-pec.fr;

Contributing authors: ouardafenek@gmail.com;

## Abstract

Requirements formalization is a critical part of any verification methodology for embedded systems like those in the automotive industry. But the needs for an intuitive and user-friendly interface for software engineers enters in direct conflict with the detailed and precise syntax of temporal logic, not to mention its semantic intricacies. Many approaches to requirement formalization use logic which is tailored for verification, just as code is tailored for simulation. So the pervasive need for code generation support, is mirrored by an endless need to produce logic formulas that prescribe safe and reliable system behavior.

However correct coding and writing correct logic are demanding, error prone and usually slow activities. One ultimate goal of software engineering could be attained if AI-supported translation could produce formal system requirements from natural language in a safe and reliable manner. We present limited but concrete progress in this direction by translating a stereotyped fragment (or pseudo-) English to, possibly metric, linear temporal logic using two approaches. The first one is a context-free grammar that mimics the temporal logic but provides much user convenience by mapping each constructor to a set of alternative grammar rules, inverse-mapping each temporal logic formula to a set of pseudo-English alternatives that is exponential in the depth of the syntax tree. This grammar maps pseudo-English sentences to temporal logic unambiguously and requires no training to use once it is defined. It has been demonstrated on hundreds of real-life examples and validated by an international patent.
But building or extending the grammar itself requires some understanding of the translation rules, and that is contrary to the objective of complete convenience or self-programming that is provided by AI techniques. To alleviate this problem, and as a second step we have built deep neural nets inspired by NLP to effectively learn the context-free grammar from its input-output examples, and thus replace it by a form of AI. This approach removes the need to write new grammar productions (or even to understand BNF notation) by retraining after the addition of new ad hoc input-output pairs.

The AI models were built from real-life and synthetic datasets and had to use a hybrid approach to overcome their initial limitations on this very "unnatural language processing". Their hybrid design combines named entity recognition with sequence-to-sequence translation. It achieved 97% accuracy on tens of thousands of examples. It can also be applied to requirements classification, which was not possible for a context-free grammar as in our first approach.

Our experiment thus combines the safety and reliability of a custom-designed grammar, the baseline reference for translation, with the convenience and flexibility of machine learning. We currently have no theoretical understanding of this specific grammar-to-AI conversion, but it qualifies as a *certainly* approximately correct (to paraphrase Leslie Valiant [1]) translation automorphism i.e. a guaranteed near-perfect isomorphism of the [pseudo-English × (M)LTL] translation graph to itself.

**Keywords:** Requirements formalization, context-free grammar, natural-language, temporal logic, machine learning, transformers, sequence-to-sequence, named-entity recognition.
# 1 Introduction

System requirements, often referred to as configurations necessary for the smooth and efficient operation of hardware or software applications, play a crucial role in ensuring optimal performance. Failure to meet these requirements can lead to installation or performance issues, with potential consequences ranging from installation failures to product malfunctions or even system crashes. Notably, such failures can have significant ramifications for businesses and, in certain cases, pose life-threatening risks. For instance, critical software errors have historically plagued aircraft and spacecraft, exemplified by the failures experienced by Boeing's airplanes and NASA's spacecraft. Given the high stakes involved, verifying system requirements before and after market release is of paramount importance. When safety-critical system requirements are formally expressed, they can be leveraged for automatic verification using solvers and model-checkers. This approach, integral to Model-Based Software Engineering due to its precision and automation, enables the rigorous analysis of interaction models. We contend that Bounded Linear Temporal Logic (BLTL), constructed from a finite set of propositional variables, logical operators such as negation ($\neg$) and dis-junction ($\vee$), temporal modal operators, and a time indicator, offers a suitable formalism for specifying and verifying properties of reactive systems.

Unfortunately, formal languages like BLTL are often complex and not intuitive, posing challenges for engineers untrained in such languages.

To harness the precision and accessibility afforded by formal requirements, we aim to simplify their creation. This study explores the feasibility of expressing requirements in natural language, which are subsequently processed to derive logical formulas. For instance, engineers could express the previous BLTL formula as follows: `(engine_stable until reply) if action and (ultimately bounded within 120 seconds)`. To achieve this, we propose a context-free grammar for articulating real-time system requirements and translating them into Linear Temporal Logic (LTL) in a clear and reversible manner. This methodology has been validated using numerous examples from the Kansas State University database of formalized requirements and is further supported by a recent patent.

However, developing or expanding such a grammar necessitates a deep understanding of the translation process. To address this challenge, we explore the use of neural networks adapted from Natural Language Processing (NLP) to learn and replace the pseudo-English-to-LTL translation, thereby enabling extension without explicit grammar use. While similar techniques have been proposed previously, their application to model-checking and their reversible nature are novel. Subsequent sections introduce the grammar-based translation approach within the context of automotive real-time systems model-checking. We describe an initial neural network, trained on a mix of real-life and synthetic datasets, followed by a more refined solution demonstrating high prediction accuracy.
## 2 From Natural Language to Temporal Logic for Real-Time Embedded Systems

The use of model-checking techniques for exploring software and system designs is now well established. It allows the formal, and possibly automatic verification of formally-defined system properties against models of their implementation that use transition system or Petri nets as formal semantics. Model-checking has been applied successfully to aerospace systems [2, 3], and more recently automotive systems, in particular to their embedded operating system [4, 5].

Safety properties of critical systems [6] can thus be verified provided their models are realistic, detailed enough, and themselves correct with respect to the final implementation. Formal specification of the system [7], most often using linear temporal logic [8] and requirements formalization of the properties [9] are the two pillars of safety-critical system verification.

So the convenience and reliability of requirements specification should not be understated. We have been inspired in this direction by the work of Dwyer et al. [10] who both collected and classified a set of several hundred requirement patterns from applied verification work. To improve convenience, some specialized requirement notations have been designed and applied [11, 12] but for the software engineer untrained in logic they can hinder productivity. We have therefore sought to use a form of natural language for requirements input, but without sacrificing safety. Some recent and more limited work in the same spirit confirms the importance of our objective [13] to connect English-like sentences to linear temporal logic for formal system verification.

### 2.1 Motivation and Context

Software errors have huge business- and life-threatening consequences while formal verification maximizes quality and provides elements for certification. Formal verification is highly recommended for embedded system products (automotive, 5G base station, critical cloud services). System requirements define the ultimate properties the user-customer wants and needs. But verification cannot happen without formal system requirements. Ambiguous requirements lead to misunderstandings and safety issues. Incoherent requirements cannot be implemented and waste design and implementation effort. However, if formalized early, the incoherences can appear as unsatisfiability that solvers can identify even before model checking.

Precise and coherent requirements lead to high quality systems. Yet requirements that are complete and precise are notoriously difficult to write, that is the challenge of requirements engineering.

Natural language requirements are easy to write and use, they increase productivity. But they can be ambiguous, imprecise and difficult to check for errors.

Temporal logic formulas are non-ambiguous, precise and can be checked by machines which leads to safety and quality. But logic is difficult to write and lowers productivity. To provide a bridge between the two languages we have invented a translation from a fragment of English to Linear Temporal Logic (LTL) [14].
## 2.2 Core Concept and Novel Aspects

The Kansas-State University database of requirement patterns by Dwyer et al [10] provided our starting point. We parsed and analyzed all 400+ patterns and ranked them by frequency. In decreasing order of frequency they are the following:

<table><tr><td>Action-reaction</td><td>G(X → F(Y))</td></tr><tr><td>Immediate reaction</td><td>G(X → Y)</td></tr><tr><td>More complex variant</td><td>A(G(X → A(F(Y))))</td></tr><tr><td>Useful special-case</td><td>G(X → F(!Y₁ ∧ F(Y₂)))</td></tr><tr><td>Absence of problem</td><td>A(G(!X))</td></tr><tr><td>Global regular variant</td><td>G(∩<sup>m</sup><sub>i=0</sub>(X → Y<sub>i</sub>))</td></tr><tr><td>A form of liveness</td><td>A(F(X ∧ Y))</td></tr></table>

where the temporal operators G, F mean "globally" (over states) and "ultimately", while A means "for every time-sequence". Those forms were the first examples for which we designed a natural-language syntax. But in the final version we tested our translation on all 400+ examples.

To strike a balance between dense but difficult to read temporal logic, ambiguous natural language, straightforward but complex automata and transition diagrams, we have designed a the direct translation of pseudo-English forms to temporal logic. The software tool for doing this was called nl2tl for "natural-language to temporal logic". It allows the user to write temporal logic formulas in a form similar to English with a large set of synonymous forms (see the appendix).

Ours is not the first attempt in this direction. Indeed the closest prior work was that of Fantechi et al. [15] and also Nelken and Francez [16] both of them dating back to the 1990s. The first paper describes a translation from natural language to ACTL temporal logic. It serves the same purpose of system requirements for formal verification and its implementation is also a grammar. But its grammar was not implicit in the publication (ours is listed here in the appendix and was part of patent [14]), did not support multiple natural-language synonyms for a given formula (our grammar proposes four different forms for negation, eight for inequality of terms etc.) and did not propose the idea of a reverse translation so that model-checking errors could be displayed in natural language. The work of Nelken and Francez is similar with an implementation that uses an NLP system dated from 1996 (hence grammar-based) and neither did it propose a reverse translation, nor did it have a proof of concept with model checking. We have surveyed 10 existing industrial tools for requirements engineering and studied the limited documents that are publicly available about them:

* Siemens Digital: Polarion requirements

* Visure solutions: visure requirements

* Jama Software: JAMA

* Innoslate: innoslate requirements

* IBM rational: requirements composer

* Techno Solutions: Topteam analyst

* Microsoft: Modern requirements (eDev Tech)

* SPARX systems: enterprise architect

* Argosim - Dassault: STIMULUS
<figure><img src="image_2.png" /><figcaption>Fig. 1: Industrial tools for requirements manipulation</figcaption></figure>

• BTC Embedded Systems: Embedded Specifier

Only the last two from Dassault and BTC support Kansas-U style universal patterns a.k.a. structured templates and possible automata-like graphical input. The input language of STIMULUS is extensible, a feature that we have also supported in the AI-powered version of our tool described in the next sections. STIMULUS supports requirements execution/simulation but not formal verification. BTC's tool [17] extracts code variables from natural language requirements but its reference input is a graphical time-sequence representation, certainly familiar to engineers but not as flexible and extensible as language. Moreover it supports no direct translation to logic formulas and needs user interaction to refine the requirements to a formal representation, thus lowering productivity. At the end of the tool chain it produces C code observers, which makes it part of a monitoring (and not verification) methodology.

2.3 Context-Free Grammar and Ad-hoc Implementation

We have designed our context-free grammar by working backwards from the LTL syntax that we wanted to produce (appendix). From keywords (eventually, milliseconds, always, etc.) and arithmetic/boolean logic (minus, and, etc.) to constructions (e.g. for all (i = a .. b) X), all forms were given multiple synonyms in pseudo-English, often more than 5. As a result a LTL expression whose syntax tree has depth 4 could have up to 5⁴ possible forms as input. Allowing any mix of mathematical expressions or english words has proven very useful in practice: "X is not equal to Y until Phi", "(X != Y) U Phi" are equally valid inputs for example. This flexibility does not come at the expense of errors because the grammar is unambiguous: only very rare input sentences can be parsed in more than one syntax tree.

To experiment freely with the grammar we have given it an ad-hoc implementation in OCaml without using a parser generator and its LALR constraints for example. This allowed us to confirm that all Kansas-state University database examples, plus several
<figure><img src="image_3.png" /><figcaption>Fig. 2: BTC's embedded specifier tool</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 3: Non-injective translation</figcaption></figure>

dozen others at our disposal from Grenoble University's VERIMAG laboratory, could be written in pseudo-English with much flexibility but absolute certainty as to their LTL translation. The pseudo-English is a formal language in disguise. Many examples of it are shown in the following sections.
<figure><img src="image_5.png" /></figure>

## 2.4 Evidence for Correct Translation

When aiming for a "correct" translation of natural language to temporal logic one is faced with the problem of informal semantics. It is not possible to prove a translation's correctness if the input language has no formal semantics. Luckily we are dealing with a small subset of English and can rely on so-called Montague semantics [18] that formalizes a small fragment of English. Special attention was given in that work to names, identity and equality, as in most of mathematical logic. We did not find a reference to the form "shall not hold" that we use as one of the synonyms for negation. But the conjugated verb to be "is" as in "X is Y" is used as a local substitution in our grammar, with the same meaning (substitution for a bound variable) that it has in most formal languages and, most importantly, in Montague semantics. Boolean and temporal operators pose no specific problems as they do not have variable binders. Relational operators can be expressed in our grammar as "is more than", "is less or equal to" etc, and this use of "is" poses no technical problem because the word "is" is not here an isolated operator but just a syntactic part of the terminal symbol "is more than".

As a result of this study of our translation rules we could conclude that, confidence in Montague semantics for the meaning of its intersection with our pseudo-English entails confidence in our translation to temporal logic. The reader familiar with programming language semantics will easily observe that, despite appearing to be a "natural" and
st: STATE_NAME. stn2: Expression. req ⊢ φ
st1 equals st2 in req ⊢ φ[ st := (stn2) ]

X of type state / term / arithmetic

<figure><img src="image_6.png" /></figure>

fn: FORMULA_NAME. req1 ⊢ φ. req2 ⊢ ψ
fn means req2 in req1 ⊢ φ[ fn := (ψ)]

<figure><img src="image_7.png" /></figure>

X of type requirement / formula

Translation rules

(*)

Basic rules

T1. (a) If x is in the domain of g, then x translates into g(x).

(b) **be translates into ∃P(x)[j[x := y]];**

(c) **necessarily translates into β[□p].**

i.e., «X is Y» in a context P means
«function of P and «X» to P's meaning
where [X: = X's meaning].

* Similar observations for Boolean/temporal operators

* English->Temporal logic examples from research papers confirm our grammars.

"free" language, our input language has much simpler semantics than "formal" modern programming languages with their inheritance, sub-typing, casting, lazy evaluation or other statically undecidable semantic traits.

## 2.5 Eclipse-Xtext Implementation

To produce a more convincing proof of concept for software engineers, we produced a second implementation of the english-to-LTL translation with Eclipse and Xtext [19, 20]. A fraction of the synonyms were removed to facilitate ANTLR-based parsing, but this was a marginal disadvantage. The resulting tool had syntax auto-completion, hovering comments, syntax-tree views, automatic input of keywords from the model-checking tool BIP (so as to use them in the formalized requirements). The main benefit of LTL translation was realized even before transfer to model checking: requirement formulas could be checked for satisfiability / joint coherence, and in case of a tautological input a warning could be issued. Non-satisfiability error- or tautology warning messages can be issued in pseudo-English so that the user may never have to read LTL formulas.

<footnote>(*) Montague, R. (1973). The proper treatment of quantification in ordinary English. In *Approaches to natural language* (pp. 221-242).
Springer, Dordrecht. Section 3 “Translating English to Intensional logic”.</footnote>
## Technical implementation details

* Based on 10-yr study of Kansas State University database of formal requirements.

* Requirements from VERIMAG University of Grenoble applied research

* Tested thousands of examples, fast translation to temporal logic, fully instrumented syntax

* Covers all known examples, easy to extend.

* Warns of useless requirements that are always true

* Warns of contradictions before formal verification

### Informal English-language requirements

<figure><img src="image_8.png" /></figure>

Automatic
&
real-time

<figure><img src="image_9.png" /></figure>

### Formal temporal logic requirements

<figure><img src="image_10.png" /></figure>

## 2.6 Domain-specific forms and grammar extensibility

Finally we explored parts of our target use-case in automotive formal requirements. In doing this, it was found useful to write more specific grammar rules that were used as shortcuts or a kind of language macros. For example a special rule allows to enter

X shall be always performed
within (t+1) ms
in case Gears_engaged does not hold

so as to produce

$$G_{\infty}((!\text{Gears\_engaged}) \rightarrow F_{(t+1)*0.001}(X)).$$

Using such grammar forms is as easy and intuitive as with the basic grammar. But there is a considerable drawback to how it was implemented: this business-case sub-language required an extra page of BNF notation (last page of the appendix) which is certainly possible for most software engineers but much less convenient than the pseudo-English. This observation led us to the AI-supported approach which we will describe in the rest of the paper. It preserves the safety and convenience of our translation while allowing extension by the simple creation of new input-output data (positive examples of translation) for retraining.

## 2.7 Motivations for Machine Learning

The current version of our translation tool operates by parsing English text, potentially overlooking minor alterations in pseudo-English constructions, leading to incomplete translations. Our forthcoming endeavor involves the development of an updated version of the translation tool leveraging machine learning techniques. This version aims to maintain robustness while accommodating subtle variations in English expressions and expanding its capacity to handle more complex formulas.
The problem at hand can be analyzed from multiple perspectives. Our exploration focuses on sequence-to-sequence translation from natural language to temporal logic. Recognizing the structured nature of logical formulas, we are also considering the incorporation of named entity recognition models to identify variables within these formulas.

# 3 Deep Learning Methods

## 3.1 RNNs based Sequence to Sequence Model with Attention Mechanism

The focus of this study appears to revolve around automatic translation, suggesting the adoption of sequence-to-sequence models. However, due to the inherently structured nature of logic formulas and their rigid syntax, the potential for outputs to closely resemble inputs becomes evident. Consequently, the integration of attention mechanisms emerges as a compelling avenue of exploration. These mechanisms offer the ability to selectively copy words from the input sequence, rather than relying solely on generative processes.

### 3.1.1 Data-Set

The dataset used for training this model comprised a combination of original data sourced from the Kansas State University database [10] and augmented data generated through various data augmentation techniques applied to the initial dataset. It contains couples (X, y) where X are the English sentences and Y their corresponding LTL formulas. 50 000 couples were used in total, which were then divided into a training set of 35 000 couples (28 000 for training and 7000 for validation) and a test set of 15 000 couples. Figure 4 describes the data.

eventually CURRENT_DISPLAY within 73 seconds; F{73} (CURRENT_DISPLAY)
ultimately PROCESS_QUEUE until ACTIVE if DOWN; F{} (DOWN -> PROCESS_QUEUE U ACTIVE)
globally D if TRIGGER and PID until TRIGGER; G{} (TRIGGER & (PID U VAR) -> F{} (D))
DRIFT * Z.UPDATE; DRIFT * Z.UPDATE
globally NPROCS until 93 seconds; G{93} (NPROCS)
idle at next time step and update; N (idle) & update
SYCHRONOUS if TRIGGER; TRIGGER -> SYCHRONOUS

<caption>Fig. 4: Data-Set Description</caption>

### 3.1.2 Architecture

By leveraging a carefully designed neural network structure, our model aims to effectively capture intricate relationships within the data while minimizing over-fitting. With its modular design and attention mechanisms, the proposed architecture demonstrates promising capabilities in handling complex forms of data. Figure 5 shows the network's layers. The model has been implemented in PyTorch, trained for 70000 steps remotely on Huawei's Paris Cluster using nvidia GPU's, with a batch size of 8.
<figure><img src="image_11.png" /><figcaption>Fig. 5: Sequence to Sequence Model Architecture</figcaption></figure>

a learning rate equal to 0.005, an *Adam* optimizer, *GRU* cells for both encoder and decoder, a hidden size of 200, an embedding dimension of 100, 3 encoder's layers, 3 decoder's layers and a dropout probability of 0.1.

As the use case of the model is related to AutoSAR domain, autonomous cars more specially, the vocabulary size was constructed of about 2000 words.

The loss function propagated was the Cross Entropy Loss. It's evolution during training is captured in Figure 6.

### 3.1.3 Results

Training accuracy reached 25.30% and test accuracy 17.29%. We have also calculated the BLEU metric which was 84.26% in train and 70.43% in test. Although the

<table><caption>**Table 1:** Sequence to Sequence Evaluation</caption><thead><tr><td>Evaluation</td><td>Train</td><td>Test</td></tr></thead><tbody><tr><td>Accuracy</td><td>25.30</td><td>17.29</td></tr><tr><td>Bleu</td><td>84.26</td><td>70.43</td></tr></tbody></table>

BLEU scores are relatively high, the accuracy remains moderate. Our analysis of this disparity indicates that most errors stem from variations in variables, while the
<figure><img src="image_12.png" /><figcaption>Fig. 6: Sequence to Sequence Loss Evolution</figcaption></figure>

structural elements are generally well learned. Illustrative translation samples derived
from the application of this model are depicted in Figure 7.

```
<en> speed and variable </en>
<tl> speed &amp; variable </tl>

<en> ultimately gears or speed within 38 seconds </en>
<exp> f { 38 } ( gears | | speed ) </exp>
<gen> f { 26 } ( state | | gears ) </gen>

<en> drift is more than g </en>
<tl> drift > g </tl>

<en> globally idle = previous_value until 97 seconds </en>
<exp> g { 97 } ( idle = = previous_value ) </exp>
<gen> g { 12 } ( idle = = idle ) </gen>
```

<caption>Fig. 7: Sequence to Sequence Translation Results</caption>

We notice that the present model has successfully learned to translate structural
elements but struggles with variable identification. Consequently, its current state
renders it unsuitable for the translation task at hand.

## 3.2 Transformers : Attention Is All You Need

In response to the previous approach's results, our attention has turned towards
transformers, which represent the cutting-edge in Natural Language Processing tasks.
Unlike Recurrent Neural Networks, transformers do not necessitate sequential data
processing in a linear fashion. This fundamental distinction means that transform-
ers can process sentences without the constraint of order, eliminating the need to
await completion of sentence beginnings before processing their endings. This inher-
ent characteristic facilitates significantly greater parallelization compared to RNNs,
consequently leading to reduced training times.

3.2.1 Data-set

The data-set used to train and test this model is the same one used with the previous
sequence to sequence model. The source sentences were English sentences and the
targeted ones were temporal logic formulas. It contains 28 000 couple for training,
7000 for validation and 15 000 test couples.

3.2.2 Architecture

The architecture follows the encoder-decoder paradigm, wherein Recurrent Neural
Networks (RNNs) are substituted with a Self Attention layer to capture sequential
dependencies, complemented by Positional Encodings. Notably, all these components
consist exclusively of fully connected (FC) layers. Given this architecture's reliance
on FC layers throughout, it facilitates straightforward parallelization, enhancing
computational efficiency. See Figure 8.

<figure><img src="image_13.png" /><figcaption>Fig. 8: Transformers Model Architecture</figcaption></figure>
The encoder is composed of a stack of $N = 6$ identical layers. Each layer has two sub-layers. The first is a multi-head self-attention mechanism, and the second is a simple, position-wise fully connected feed-forward network. We employ a residual connection [?] around each of the two sub-layers, followed by layer normalization [?]. To facilitate these residual connections, all sub-layers in the model, as well as the embedding layers, produce outputs of dimension $d_{model} = 512$. The decoder is also composed of a stack of $N = 6$ identical layers. In the "Scaled Dot-Product Attention" module, the input consists of queries and keys of dimension $d_k = 64$, and values of dimension $d_v = 64$. Instead of performing a single attention function with $d_{model} - dimensional$ keys, values and queries, we found it beneficial to linearly project the queries, keys and values $h = 8$ times with different, learned linear projections to $d_k$, $d_k = d_q$ and $d_v$ dimensions, respectively. For the position-wise Feed-Forward network, the dimension of input and output is $d_{model} = 512$, and the inner-layer has dimension $d_{inner} = 2048$. We have used an *Adam* optimizer with a learning rate = $10^{-9}$, 12800 warmup steps, $\beta_1 = 0.9$ and $\beta_2 = 0.98$. Finally we set the batch_size = 32. It has been implemented in *PyTorch* and trained remotely on Huawei's Paris Cluster for 50000 steps. The loss and perplexity evolutions are captured in Figure 9.

<figure><img src="image_14.png" /><figcaption>Fig. 9: Transformers Loss and Perplexity Evolution</figcaption></figure>

### 3.2.3 Results

<table><caption>**Table 2:** Transformers Evaluation</caption><thead><tr><th>Evaluation</th><th>Train</th><th>Test</th></tr></thead><tbody><tr><td>Accuracy</td><td>40.78</td><td>38.89</td></tr><tr><td>Bleu</td><td>69.91</td><td>67.08</td></tr></tbody></table>

The integration of transformers resulted in an enhancement of the accuracy metric in contrast to the preceding sequence-to-sequence model. Nevertheless, achieving a 40% accuracy rate is deemed notably subpar. Figure 10 shows a sample of the obtained translations applying this model.
<figure><img src="image_15.png" /><figcaption>Fig. 10: Transformers Translations Results</figcaption></figure>

## 3.3 Hybrid Solution: Named Entity Recognition and Sequence to Sequence with Attention Mechanism

Upon comparing the results of our previous experiments, we observed that despite the lower accuracy of the RNN-based Sequence-to-Sequence model, its outputs exhibit a discernible pattern absent in the transformer outputs. Specifically, the RNN-based model effectively learns structural elements but tends to confuse variables. Consequently, we propose the development of a hybrid model. Initially, a Named Entity Recognition (NER) model to identify and categorize entities that are the variables of the formula. Subsequently, these entities are replaced with a predefined set of patterns, thereby reducing the vocabulary size. The revised dataset is then used to train the same RNN-based Sequence-to-Sequence model with Attention Mechanism, with a focus on learning structural patterns within the context of the simplified vocabulary.

### 3.3.1 Named Entity Recognition Data-set

To address the entity recognition component, a dedicated dataset was created for the task. We conducted manual analysis of recurring patterns within the structures and subsequently generated annotated data based on the identified rules. The dataset comprises pairs $(X, y)$, where $X$ represents English sentences and $y$ denotes the corresponding entities. Each entity is characterized by its type and position within the sentence like described in Figure 11. In total, the dataset consisted of 63,500 pairs, which were partitioned into 44,450 for training and 19,050 for testing purposes.
<figure><img src="image_16.png" /><figcaption>Fig. 11: NER Data-set Sample</figcaption></figure>

### 3.3.2 Named Entity Recognition Model

This model was trained using SpaCy. The training focused on two entities: CAR-DINAL, responsible for detecting numerals, and a newly introduced entity named LEAF, designed to encompass all variables. We fine-tuned the pre-existing model *en_core_web_sm* for 400 steps, employing a dropout rate of 0.5. The training used SpaCy's utility function *compounding* that allows changes on the batch size during the process. It started at 4 and progressively increased to reach 32. The loss evolution is captured in 12.

<figure><img src="image_17.png" /><figcaption>Fig. 12: NER Loss Evolution</figcaption></figure>

### 3.3.3 Named Entity Recognition Results

To assess this model, we assessed its precision, representing the proportion of relevant instances within the retrieved ones, and recall, indicating the fraction of all relevant instances successfully retrieved. Subsequently, we computed the F1 score, a metric derived from the harmonic mean of precision and recall. A perfect F1 score, achieving 1, indicates both perfect precision and recall.
<table><caption>**Table 3: NER**
Evaluation</caption><thead><tr><th>Evaluation</th><th>Train</th><th>Test</th></tr></thead><tbody><tr><td>Precision</td><td>100</td><td>99.99</td></tr><tr><td>Recall</td><td>100</td><td>100</td></tr><tr><td>F1</td><td>100</td><td>99.99</td></tr></tbody></table>

Figure 13 provides a representative sample of our experimental results, shedding light on the efficacy of the fine tuned Spacy NER model.

<figure><img src="image_18.png" /><figcaption>**Fig. 13: NER Results Sample**</figcaption></figure>

### 3.3.4 Pre-Processing Before Sequence to Sequence

Once our Named Entity Recognition (NER) Model had been trained, we proceeded to deploy it on the original dataset comprising English sentences and Linear Temporal Logic (LTL) formulas. The objective was to extract all leaf nodes and numerical values. A detailed overview of this preprocessing step is provided in Figure 14.

Following this, each sentence underwent a transformation wherein the identified leaf nodes were systematically replaced with a finite set of tokens such as "v1," "v2," "v3," "v4," etc., in the order of their occurrence. Simultaneously, numerical values were substituted with the token "value". This systematic process led to a substantial reduction in the vocabulary size, culminating in a concise set of only 90 tokens. For a visual representation of the resulting dataset, refer to Figure 15.

### 3.3.5 Sequence to Sequence Training

We have trained the model described in figure 5 on the new data-set in figure 15 for 35000 steps with a batch size of 8, a learning rate of 0.005, a hidden size equal to
<figure><img src="image_19.png" /><figcaption>**Fig. 14:** Hybrid Solution: NER + Sequence to Sequence - Pre-Processing Description -</figcaption></figure>

```
globally ( v1 holds ultimately ) if v2 ; G{}( v2 -> F{} ( v1 )
globally v1 until v2 if v3 ; G{} ( v3 -> v1 U v2 )
ultimately v1 until v2 if v3 ; F{} ( v3 -> v1 U v2 )
globally v1 if v2 and v3 until v4 ; G{} ( v2 & ( v3 U v4 ) -> F{} ( v1 ) )
( v1 until v2 ) if v3 and ( ultimately v4 ) ; G{} ( ( v3 & F{} ( v4 ) ) -> ( v1 U v2 ) )
if v1 is v2 then it is never v3 ; v1 == v2 -> G{} ( v1 != v3 )
when v1 shall be true v2 shall be true ; G{} ( v1 -> F{} ( v2 )
when v1 does not hold v2 does not hold ; G{} ( ! ( v1 ) -> F{} ( ! ( v2 ) ) )
```

<caption>**Fig. 15:** Processed Data-Set Description</caption>

200, an embedding dimension of 100, a dropout probability of 0.1, 3 layers for each RNN, we used the optimizer Adam and chosen the RNN cells to be GRU ones. Loss evolution is captured in figure 16.

<figure><img src="image_20.png" /><figcaption>**Fig. 16:** Sequence to Sequence Training - Learning Structures</figcaption></figure>
### 3.3.6 Results

The evaluation metrics reported in Table 4 exhibit elevated values in both the training and testing phases, indicating strong performance across the model's learning and generalization capabilities. Figure 17 shows a representative sample of its results.

<table><caption>**Table 4:** Sequence to Sequence Model Learning Structures</caption><thead><tr><td>Evaluation</td><td>Train</td><td>Test</td></tr></thead><tbody><tr><td>Accuracy</td><td>98.70</td><td>97.16</td></tr><tr><td>Bleu</td><td>98.01</td><td>95.89</td></tr></tbody></table>

<figure><img src="image_21.png" /><figcaption>**Fig. 17:** Seq2Seq Learning Structures - Results Sample</figcaption></figure>

### 3.3.7 Post-Processing and Final Results

After identifying the entities, substituting them, and translating the structural elements, the subsequent step involves replacing the temporary variables in the target language with their original values from the English sentences. This finalizes the translation process, resulting in the complete translation. A sample of the final translation results is in figure 18.

## 4 Discussion

The forthcoming figure 19 provides a comprehensive summary of the outcomes derived from the experiments conducted for this task. It encapsulates evaluation of the Deep Learning three methodologies. It is noteworthy that by building a hybrid model, we
<figure><img src="image_22.png" /><figcaption>Fig. 18: Final Results Sample</figcaption></figure>

have achieved a favorable accuracy level of 97%. As such, this refined model stands as our definitive submission for addressing the given task.

## 5 Conclusion

We have demonstrated a new approach to requirements formalization that combines the simplicity and user friendliness of a fragment of English, with the reliability of a context-free translation to temporal logic. The mapping to logical operators is many-to-one (with multiple synonyms) but without ambiguity. The language is immediately and safely usable by an untrained user, but in its grammar form is not extensible without grammar "coding". To alleviate this drawback we have produced large datasets of translation examples, then designed an AI-powered NLP implementation that (in its final form) reproduces almost perfectly the grammar's translation, with reasonable training times. The AI implementation, by its very nature avoids the need to write any new grammar rules in case an extension is needed. Having internalized the grammar in its neural nets it can be extended by retraining with new dataset elements that express new specific rules.

We have no deep theoretical understanding of this whole experiment but have learned the following interesting dimensions of the problem.

First of all, the context free grammar that serves our purpose is neither that of a usual formal logic or programming language, with its left-to-right constraints, operator priorities and possible parentheses, but a seemingly free-form context-free grammar. However the grammar's form follows a simple pattern: a set of synonymous rules that map the same set of input sub-phrases to a formula with a given logical operator. Using this method we find only very rare ambiguities in parsing.

Secondly the Sequence-to-Sequence model could reproduce our target LTL syntax trees almost perfectly but with the wrong leaves: correct logical operators at the correct
<figure><img src="image_23.png" /><figcaption>Fig. 19: Methods Results Summary</figcaption></figure>

places but strange permutations of constants or variables at the leaves. This intriguing phenomenon was compensated by adding a Named Entity Recognition model that can reproduce the list of syntax tree terminals, without learning the internal nodes i.e. the logical operators. Together the two models produce a near perfect translation, having learned the two parts of the grammar.

Finally on a more abstract level we find that our experiment is a special case yet positive example of Valiant's philosophy for machine learning. Following his fundamental contributions in computational complexity, parallel computing models and machine learning his essay "Probably approximately correct ..." [1] relates the Computer Science of probabilistic - approximate computing with how nature produces learning creatures such as ourselves. Approximate algorithms have been known for long and most machine-learning AI computing today is probabilistic.

In this mental grid we can position our work as follows. The initial grammar defines a very specific and useful translation graph from pseudo-English to temporal logic. In it, many sentences map to a single temporal logic formula, and so recursively. This infinite graph is our proposed table for facilitating requirements formalization. It is large but not extensible in itself. Deep learning NLP gives us an automorphism on this graph: it is approximately correct (a very small percentage of errors) and this does not happen probably, as in Valiant's slogan, but certainly. The automorphism is an encoding of every context-free production in the weights of its neural nets that serve to reproduce the translation. But as automorphisms are groups they preserve composition and inverses.

Since adding manually context-free rules can be reproduced by DL-NLP, the latter
could also produce new context-free rules if given enough new input-output transla-
tion examples. We hope that this general concept can lead to further studies and a
deeper understanding of how probabilistic AI can lead to more certainty in software
engineering.

**Supplementary information.**

**Acknowledgments.** The first author thanks Saddek Bensalem for introducing him to the research field of requirements formalization.

**Declarations**

**5.1 Funding**

The work described here was funded by Huawei Technologies France while the first author was Principal Engineer and second author was MSc intern from Université Paris Sorbonne.

**5.2 Competing interests**

Not applicable.

5.3 Ethics approval

Not applicable.

5.4 Consent to participate

Not applicable.

**5.5 Consent for publication**

Not applicable.

**5.6 Availability of data and materials**

Training data is available upon request.

**5.7 Code availability**

Python source code and trained AI models are subject to restrictions.

**5.8 Authors' contributions**

The first author contributed the temporal-logic from natural-language grammar,
implementation and the training datasets. The second author contributed the machine-
learning models, training and post-processing.
References

[1] Valiant, L.: Probably Approximately Correct: Nature's Algorithms for Learning and Prospering in a Complex World. Basic Books (AZ), New-York (2013)

[2] Havelund, K., Lowry, M., Penix, J.: Formal analysis of a space craft controller using SPIN. Technical report, NASA Ames Research Center, Recom Technologies, Moffet Field (1998)

[3] Alspaugh, T., Faulk, S., Britton, K., Parker, R., Parnas, D., Shore, J.: Software Requirements for the A-7E Aircraft. Technical report, Naval Research Laboratory (March 1988)

[4] Béchennec, J.-L., Roux, O.H., Tigori, T.: Formal model-based conformance verification of an OSEK/VDX compliant RTOS. In: 2018 5th International Conference on Control, Decision and Information Technologies (CoDIT). IEEE, Thessaloniki, Greece (2018)

[5] Haur, I., Béchennec, J.-L., H. Roux, O.: Formal verification process of the compliance of a multicore autosar os. Software Quality Journal 31(2), 497-531 (2023)

[6] Cimatti, A., Giunchiglia, F., Mongardi, G., Torielli, F., Traverso, P.: Model checking safety critical software with SPIN: an application to a railway interlocking system. In: Proceedings of the Third SPIN Workshop (1997)

[7] Mahmud, N., Seceleanu, C., Ljungkrantz, O.: Specification and semantic analysis of embedded systems requirements: From description logic to temporal logic. In: SEFM2017. Springer, Trento, Italy (2017)

[8] Emerson, E.A.: Temporal and modal logic. In: Formal Models and Semantics, pp. 995-1072. Elsevier, Utrecht, Netherlands (1990)

[9] Ortel, M., al.: In: Rajan, A., Wahl, T. (eds.) Requirements Engineering. Springer, Vienna (2013)

[10] M.Dwyer, Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: ICSE99. ACM, Los Angeles, USA (1999)

[11] Autili, M., Inverardi, P., Pelliccione, P.: A scenario based notation for specifying temporal properties. In: Proceedings of the 2006 International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools, pp. 21-28. ACM, ??? (2006)

[12] Roşu, G., Bensalem, S.: Allen linear (interval) temporal logic-translation to ltl and monitor synthesis. In: International Conference on Computer Aided Verification, pp. 263-277 (2006). Springer
[13] Fuggitti, F., Chakraborti, T.: Nl2ltl-a python package for converting natural language (nl) instructions to linear temporal logic (ltl) formulas. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 37, pp. 16428–16430 (2023)

[14] HUAWEI TECH CO LTD [CN]; HAINS GAETAN JOSEPH DANIEL ROBERT [DE]: Appareil et procédé de génération de spécifications d'exigences. Aparatus and method for generating requirement specification. European Patent Office. Patent number WO2022218549A1. https://worldwide.espacenet.com/patent/search/family/075588216/\publication/WO2022218549A1?q=GAETAN%20HAINS

[15] Fantechi, A., Gnesi, S., Ristori, G., Carenini, M., Vanocchi, M., Moreschini, P.: Assisting requirement formalization by means of natural language translation. Formal Methods in System Design 4, 243–263 (1994)

[16] Nelken, R., Francez, N.: Automatic translation of natural language system specifications into temporal logic. In: Computer Aided Verification: 8th International Conference, CAV’96 New Brunswick, NJ, USA, July 31–August 3, 1996 Proceedings 8, pp. 360–371 (1996). Springer

[17] Teige, T., Eggers, A., Scheibler, K., Stasch, M., Brockmeyer, U., Holberg, H.J., Bienmüller, T.: Two decades of formal methods in industrial products at btc embedded systems. In: Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20–26, 2021, Proceedings 24, pp. 725–729 (2021). Springer

[18] Montague, R.: The proper treatment of quantification in ordinary english. In: Approaches to Natural Language: Proceedings of the 1970 Stanford Workshop on Grammar and Semantics, pp. 221–242 (1973). Springer

[19] Burnette, E.: Eclipse IDE Pocket Guide: Using the Full-Featured IDE. " O’Reilly Media, Inc.", Sebastopol, CA 95472, USA (2005)

[20] Eysholdt, M., Behrens, H.: Xtext: implement your language faster than the quick and dirty way. In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, pp. 307–309 (2010)

[21] Bensalem, S.: Statistical Model Checking QoS properties of Systems with SBIP. Technical report, CNRS (2013). https://hal.archives-ouvertes.fr/hal-00847827
Appendix: Context-free grammar

//*() : term
[basic_term] ::= <term_name>. {term_name_of_arg1}

//(Number _): term

[basic_term] ::= <number>. {Number -1}

//(_): term

[basic_term] ::= "(" [term] ")". {Term_name $2}

//Fun1(_,_): term

[basic_term] ::= <term_name> "(" [term] ")".
{Fun1($1,(Term_name $3))}

[basic_term] ::= <term_name> "of" [term].

{Fun1($1,(Term_name $3))}

[basic_term] ::= <term_name> "applied" "to" [term].

{Fun1($1,(Term_name $4))}

//Fun2(_,_): term

[basic_term] ::= <term_name> "(" [term] "," [term] ")".

{Fun2($1,(Term_name $3),(Term_name $5))}

[basic_term] ::= <term_name> "applied" "to" "(" [term] "," [term] ")".

{Fun2($1,(Term_name $5),(Term_name $7))}

[basic_term] ::= <term_name> "applied" "to" [term] "and" [term].

{Fun2($1,(Term_name $4),(Term_name $6))}

[basic_term] ::= <term_name> "of" "(" [term] "," [term] ")".

{Fun2($1,(Term_name $4),(Term_name $6))}

[basic_term] ::= <term_name> "of" [term] "and" [term].

{Fun2($1,(Term_name $3),(Term_name $5))}

//Abs(_): term

[basic_term] ::= "abs" "(" [term] ")".

{Abs (Term_name $3)}

[basic_term] ::= "abs" "of" [term].

{Abs (Term_name $3)}

[basic_term] ::= "absolute" "value" [term].

{Abs (Term_name $3)}

[basic_term] ::= "absolute" "value" "of" [term].

{Abs (Term_name $4)}

//Indexed(_,_): term

[basic_term] ::= <term_name> "[" [term] "]".

{Indexed($1, (Term_name $3))}

[basic_term] ::= <term_name> "at" [term].

{Indexed($1, (Term_name $3))}

[basic_term] ::= <term_name> "indexed" [term].

{Indexed($1, (Term_name $3))}

[basic_term] ::= <term_name> "index" [term].

{Indexed($1, (Term_name $3))}

[basic_term] ::= "element" [term] "of" <term_name>.

{Indexed($4, (Term_name $2))}
[multerm] ::= [basic_term]. {Term_name $1}

//Times(_,_): term

[multerm] ::= [basic_term] "*" [multerm].

{Times((Term_name $1),(Term_name $3))}

[multerm] ::= [basic_term] "x" [multerm].

{Times((Term_name $1),(Term_name $3))}

[multerm] ::= [basic_term] "times" [multerm].

{Times((Term_name $1),(Term_name $3))}

[multerm] ::= [basic_term] "multiplied" "by" [multerm].

{Times((Term_name $1),(Term_name $4))}

//Div(_,_): term

[multerm] ::= [basic_term] "/" [multerm].

{Div((Term_name $1),(Term_name $3))}

[multerm] ::= [basic_term] "over" [multerm].

{Div((Term_name $1),(Term_name $3))}

[multerm] ::= [basic_term] "divided" "by" [multerm]. {Div((Term_name $1),(Term_name $4))}

//To do: special cases "one half", "two thirds" etc.

[term] ::= [multerm]. {Term_name $1}

//Plus(_,_): term

[term] ::= [multerm] "+" [term].

{Plus((Term_name $1),(Term_name $3))}

[term] ::= [multerm] "plus" [term].

{Plus((Term_name $1),(Term_name $3))}

[term] ::= [multerm] "added" "to" [term]. {Plus((Term_name $1),(Term_name $4))}

//Minus(_,_): term

[term] ::= "-" [term].

{Minus((Number 0),(Term_name $2))}

[term] ::= "minus" [term].

{Minus((Number 0),(Term_name $2))}

[term] ::= [multerm] "-" [term].

{Minus((Term_name $1),(Term_name $3))}

[term] ::= [multerm] "minus" [term].

{Minus((Term_name $1),(Term_name $3))}

[term] ::= [multerm] "subtracted" "from" [term]. {Minus((Term_name $4),(Term_name $1))}

//*(): formula

[basic_formula] ::= "(" [formula] ")".

{Formula_name $2}

//* (Formula_name _): formula

[basic_formula] ::= <formula_name>.

{Formula_name $1}

//Eq(_,_): formula

[basic_formula] ::= [term] "=" [term].

{Eq((Term_name $1),(Term_name $3))}
[basic_formula] ::= [term] "is" [term].
{Eq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "equals" [term].
{Eq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "is" "equal" "to" [term].
{Eq((Term_name $1),(Term_name $5))}

[basic_formula] ::= [term] "is" "the" "same" "as" [term].
{Eq((Term_name $1),(Term_name $6))}

[basic_formula] ::= [term] "and" [term] "are" "equal".
{Eq((Term_name $1),(Term_name $3))}

//Neq($_, _): formula
[basic_formula] ::= [term] "!=" [term].
{Neq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "is" "not" [term].
{Neq((Term_name $1),(Term_name $4))}

[basic_formula] ::= [term] "does" "not" "equal" [term].
{Neq((Term_name $1),(Term_name $5))}

[basic_formula] ::= [term] "is" "not" "equal" "to" [term].
{Neq((Term_name $1),(Term_name $6))}

[basic_formula] ::= [term] "is" "different" "from" [term].
{Neq((Term_name $1),(Term_name $5))}

[basic_formula] ::= [term] "and" [term] "are" "not" "equal".
{Neq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "and" [term] "are" "unequal".
{Neq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "and" [term] "are" "different".
{Neq((Term_name $1),(Term_name $3))}

//Lt($_, _): formula
[basic_formula] ::= [term] "<" [term].
{Lt((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "is" "less" "than" [term].
{Lt((Term_name $1),(Term_name $5))}

// Leq($_, _): formula
[basic_formula] ::= [term] "<=" [term].
{Leq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "is" "less" "than" "or" "equal" "to" [term].
{Leq((Term_name $1),(Term_name $8))}

[basic_formula] ::= [term] "is" "no" "more" "than" [term].
{Leq((Term_name $1),(Term_name $6))}

[basic_formula] ::= [term] "is" "at" "most" [term].
{Leq((Term_name $1),(Term_name $5))}

// Gt($_, _): formula
[basic_formula] ::= [term] ">" [term].
{Gt((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "is" "greater" "than" [term].
{Gt((Term_name $1),(Term_name $5))}
[basic_formula] ::= [term] "is" "more" "than" [term].
{Gt((Term_name $1),(Term_name $5))}

// Geq($_, _): formula

[basic_formula] ::= [term] ">=" [term].
{Geq((Term_name $1),(Term_name $3))}

[basic_formula] ::= [term] "is" "no" "less" "than" [term].
{Geq((Term_name $1),(Term_name $6))}

[basic_formula] ::= [term] "is" "more" "than" "or" "equal" "to" [term].
{Geq((Term_name $1),(Term_name $8))}

[basic_formula] ::= [term] "is" "at" "least" [term].
{Geq((Term_name $1),(Term_name $5))}

[conj_formula] ::= [basic_formula].
{Formula_name $1}

// f is true: formula

[conj_formula] ::= [basic_formula] "holds".
{Formula_name $1}

[conj_formula] ::= [basic_formula] "is" "true".
{Formula_name $1}

[conj_formula] ::= [basic_formula] "shall" "be" "true". {Formula_name $1}

[conj_formula] ::= "it" "is" "true" "that" [conj_formula]. {Formula_name $5}

// to do: allow meta-language to generalize "is" to <En.to_be>

// Negation(_): formula

[conj_formula] ::= "!" [conj_formula].
{Negation (Formula_name $2)}

[conj_formula] ::= "not" [conj_formula].
{Negation (Formula_name $2)}

[conj_formula] ::= [basic_formula] "does" "not" "hold". {Negation (Formula_name $1)}

[conj_formula] ::= [basic_formula] "is" "false".
{Negation (Formula_name $1)}

// to do: allow meta-language to generalize "is"

// Conjunction(_,_): formula

[conj_formula] ::= [basic_formula] "&&" [conj_formula].
{Conjunction((Formula_name $1),(Formula_name $3))}

[conj_formula] ::= [basic_formula] "and" [conj_formula].
{Conjunction((Formula_name $1),(Formula_name $3))}

[conj_formula] ::= [basic_formula] "and" "also" [conj_formula].
{Conjunction((Formula_name $1),(Formula_name $4))}

// Qconjunction(_,_:_): formula

[conj_formula] ::= "&&" "{" <term_name> "=" [term] ".." [term] "}" [conj_formula].
{Qconjunction($3,(Term_name $5),(Term_name $7),(Formula_name $9))}

[conj_formula] ::= "for" <term_name> "=" [term] ".." [term] [conj_formula].
{Qconjunction($2,(Term_name $4),(Term_name $6),(Formula_name $7))}

[conj_formula] ::= "for" "every" <term_name> "=" [term] ".." [term] [conj_formula].
{Qconjunction($3,(Term_name $5),(Term_name $7),(Formula_name $8))}
[conj_formula] ::= "for" "all" <term_name> "=" [term] ".." [term] [conj_formula].

{Qconjunction($3, (Term_name $5), (Term_name $7), (Formula_name $8))}

[conj_formula] ::= "for" <term_name> "from" [term] "to" [term] [conj_formula].

{Qconjunction($2, (Term_name $4), (Term_name $6), (Formula_name $7))}

[conj_formula] ::= "for" "every" <term_name> "from" [term] "to" [term] [conj_formula].

{Qconjunction($3, (Term_name $5), (Term_name $7), (Formula_name $8))}

[conj_formula] ::= "for" "all" <term_name> "from" [term] "to" [term] [conj_formula].

{Qconjunction($3, (Term_name $5), (Term_name $7), (Formula_name $8))}

[conj_formula] ::= [basic_formula] "&&" "{" <term_name> "=" [term] ".." [term] "}".

{Qconjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}

[conj_formula] ::= [basic_formula] "for" <term_name> "=" [term] ".." [term].

{Qconjunction($3, (Term_name $5), (Term_name $7), (Formula_name $1))}

[conj_formula] ::= [basic_formula] "for" "every" <term_name> "=" [term] ".." [term].

{Qconjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}

[conj_formula] ::= [basic_formula] "for" "all" <term_name> "=" [term] ".." [term].

{Qconjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}

[conj_formula] ::= [basic_formula] "for" <term_name> "from" [term] "to" [term].

{Qconjunction($3, (Term_name $5), (Term_name $7), (Formula_name $1))}

[conj_formula] ::= [basic_formula] "for" "every" <term_name> "from" [term] "to" [term].

{Qconjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}

[conj_formula] ::= [basic_formula] "for" "all" <term_name> "from" [term] "to" [term].

{Qconjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}

[disj_formula] ::= [conj_formula].

{Formula_name $1}

// Disjunction(_,_): formula

[disj_formula] ::= [conj_formula] "||" [disj_formula].

{Disjunction((Formula_name $1), (Formula_name $3))}

[disj_formula] ::= [conj_formula] "or" [disj_formula].

{Disjunction((Formula_name $1), (Formula_name $3))}

[disj_formula] ::= [conj_formula] "or" "otherwise" [disj_formula].

{Disjunction((Formula_name $1), (Formula_name $4))}

[for_some] ::= "for" "some". {}

[for_some] ::= "for" "an". {}

[for_some] ::= "for" "a". {}

// Qdisjunction(_,_:_): formula

[disj_formula] ::= "||" "{" <term_name> "=" [term] ".." [term] "}" [disj_formula].

{Qdisjunction($3, (Term_name $5), (Term_name $7), (Formula_name $9))}

[disj_formula] ::= [for_some] <term_name> "=" [term] ".." [term] [disj_formula].

{Qdisjunction($2, (Term_name $4), (Term_name $6), (Formula_name $7))}

[disj_formula] ::= [for_some] <term_name> "in" [term] ".." [term] [disj_formula].

{Qdisjunction($2, (Term_name $4), (Term_name $6), (Formula_name $7))}

[disj_formula] ::= [for_some] <term_name> "between" [term] "and" [term] [disj_formula].

{Qdisjunction($2, (Term_name $4), (Term_name $6), (Formula_name $7))}

[disj_formula] ::= [conj_formula] "holds" "||" "{" <term_name> "=" [term] ".." [term] "}".
{Qdisjunction($5, (Term_name $7), (Term_name $9), (Formula_name $1))}
[disj_formula] ::= [conj_formula] "holds" [for_some] <term_name> "=" [term] ".." [term].
{Qdisjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}
[disj_formula] ::= [conj_formula] "holds" [for_some] <term_name> "in" [term] ".." [term].
{Qdisjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}
[disj_formula] ::= [conj_formula] "holds" [for_some] <term_name> "between" [term] "and" [term].
{Qdisjunction($4, (Term_name $6), (Term_name $8), (Formula_name $1))}

// Implication(_,_): formula
[if] ::= "if" {}
[if] ::= "If" {}
[disj_formula] ::= [conj_formula] "->" [disj_formula].
{Implication((Formula_name $1), (Formula_name $3))}
[disj_formula] ::= [conj_formula] "=>" [disj_formula].
{Implication((Formula_name $1), (Formula_name $3))}
[disj_formula] ::= [conj_formula] "whenever" [disj_formula].
{Implication((Formula_name $3), (Formula_name $1))}
[disj_formula] ::= [conj_formula] "if" [disj_formula].
{Implication((Formula_name $3), (Formula_name $1))}
[disj_formula] ::= [if] [conj_formula] "then" [disj_formula].
{Implication((Formula_name $2), (Formula_name $4))}
[disj_formula] ::= [conj_formula] "implies" [disj_formula].
{Implication((Formula_name $1), (Formula_name $3))}
[disj_formula] ::= [conj_formula] "implies" "that" [disj_formula].
{Implication((Formula_name $1), (Formula_name $4))}

// A(_): formula
// To do when the abstract syntax of formula will cover A.
// [formula] ::= [formula] "always". {}
// [formula] ::= [formula] "always" "holds". {}
// [formula] ::= "always" [formula]. {}
// [formula] ::= "it" "always" "holds" "that" [formula]. {}
// [formula] ::= "it" "is" "always" "true" "that" [formula]. {}

[temporal_formula] ::= [disj_formula]. {Formula_name $1}
[time_unit] ::= "seconds". {}
[time_unit] ::= "miliseconds". {}
[time_unit] ::= "mili-seconds". {}
[time_unit] ::= "s". {}
[time_unit] ::= "ms". {}
[time_unit] ::= "time" "steps". {}
[time_unit] ::= "time" "units". {}

// G(_,_): formula
[temporal_formula] ::= "G" [temporal_formula].
{G(infinity, (Formula_name $2))}
[temporal_formula] ::= "G" "{" [term] "}" [temporal_formula]. {G(-3, (Formula_name $5))}
[temporal_formula] ::= "G" "{" [term] [time_unit] "}" [temporal_formula].
{G(-3, (Formula_name $6))}
[temporal_formula] ::= "globally" [temporal_formula].
{G(infinity, (Formula_name $2))}
[temporal_formula] ::= "globally" [temporal_formula] "until" [term] [time_unit].
{G(-4, (Formula_name $2))}
[temporal_formula] ::= [disj_formula] "globally".
{G(infinity, (Formula_name $1))}
[temporal_formula] ::= [disj_formula] "globally" "until" [term] [time_unit].
{G(-4, (Formula_name $1))}
// Later: generalize "seconds" and cover more forms for this constructor.
// more delicate to implement: (... always equals ...) -recognized-> G( ... = ...)

[eventually] ::= "F". {}
[eventually] ::= "eventually". {}
[eventually] ::= "Eventually". {}
[eventually] ::= "ultimately". {}
[eventually] ::= "Ultimately". {}
[eventually] ::= "finally". {}
[eventually] ::= "Finally". {}

// F(_,_): formula
[temporal_formula] ::= [eventually] [temporal_formula].
{F(infinity, (Formula_name $2))}
[temporal_formula] ::= [disj_formula] [eventually].
{F(infinity, (Formula_name $1))}
[temporal_formula] ::= [eventually] "{" [term] "}" [temporal_formula].
{F(-3, (Formula_name $5))}
[temporal_formula] ::= [eventually] "{" [term] [time_unit] "}" [temporal_formula].
{F(-3, (Formula_name $6))}
[temporal_formula] ::= [eventually] [temporal_formula] "within" [term] [time_unit].
{F(-4, (Formula_name $2))}
// Later: generalize "seconds", factorize rules and add more.

// N(_): formula
[temporal_formula] ::= "N" [temporal_formula].
{N (Formula_name $2)}
[temporal_formula] ::= "next" [temporal_formula].
{N (Formula_name $2)}
[temporal_formula] ::= [disj_formula] "next".
{N (Formula_name $1)}
[temporal_formula] ::= [disj_formula] "at" "next" "time" "step". {N (Formula_name $1)}

// U(_,_): formula
[temporal_formula] ::= [disj_formula] "U" [temporal_formula].
{U((Formula_name $1), infinity, (Formula_name $3))}
[temporal_formula] ::= [disj_formula] "U" "{" [term] "}" [temporal_formula].
{U((Formula_name $1), -4, (Formula_name $6))}
[temporal_formula] ::= [disj_formula] "U" "{" [term] [time_unit] "}" [temporal_formula].
{U((Formula_name $1), -4, (Formula_name $7))}
[temporal_formula] ::= [disj_formula] "until" [temporal_formula].
{U((Formula_name $1), infinity, (Formula_name $3))}
[temporal_formula] ::= [disj_formula] "until" [temporal_formula]
```
"but" "no" "longer" "than" [term] [time_unit].
{U((Formula_name $1), -8, (Formula_name $3))}
// Later: generalize "seconds", factorize, add more rules.
```

```hkl
// R(_,_): formula
[temporal_formula] ::= [disj_formula] "R" [temporal_formula].
                       {R((Formula_name $1), infinity, (Formula_name $3))}
[temporal_formula] ::= [disj_formula] "R" "{" [term] "}" [temporal_formula].
                       {R((Formula_name $1), -4, (Formula_name $6))}
[temporal_formula] ::= [disj_formula] "R" "{" [term] [time_unit] "}" [temporal_formula].
                       {R((Formula_name $1), -4, (Formula_name $7))}
[temporal_formula] ::= [disj_formula] "release" [temporal_formula].
                       {R((Formula_name $1), infinity, (Formula_name $3))}
[temporal_formula] ::= [disj_formula] "until" "possibly" [temporal_formula].
                       {R((Formula_name $1), infinity, (Formula_name $4))}
[temporal_formula] ::= [disj_formula] "until" [formula] "possibly" "happens".
                       {R((Formula_name $1), infinity, (Formula_name $3))}
[temporal_formula] ::= [disj_formula] "until" "possibly"
                       [temporal_formula] "but" "no" "longer" "than" [term] [time_unit].
                       {R((Formula_name $1), -9, (Formula_name $4))}
[temporal_formula] ::= [disj_formula] "until" [temporal_formula]
                       "possibly" "happens" "but" "no" "longer" "than" [term] [time_unit].
                       {R((Formula_name $1), -10, (Formula_name $3))}
// Later: generalize "seconds", factorize, add more rules.
```

```hkl
[formula] ::= [temporal_formula].
             {Formula_name $1}
[formula] ::= "when" [conj_formula] "do" [conj_formula].
             {G(infinity, Implication((Formula_name $2), (F(infinity, (Formula_name $4))))))}
[formula] ::= "when" [conj_formula] "do" [conj_formula] "shall" "be" "true".
             {G(infinity, Implication((Formula_name $2), (F(infinity, (Formula_name $4))))))}
[formula] ::= "when" [conj_formula] "do" [conj_formula] "within" [term] [time_unit].
             {G(infinity, Implication((Formula_name $2), (F(-6, (Formula_name $4))))))}
[formula] ::= "when" [conj_formula] "do" [conj_formula]
             "shall" "be" "true" "within" [term] [time_unit].
             {G(infinity, Implication((Formula_name $2), (F(-9, (Formula_name $4))))))}
```

### Special-purpose syntax for automotive examples.

```hkl
// A complete gear change shall be always performed within 1500 ms in the case of no error.
// G(infinity, !ERROR -> F(1500, COMPLETE_GEAR_CHANGE))
//COMPLETE_GEAR_CHANGE shall be always performed within 1500 ms in the case ERROR does not hold.
[shall_be_always_performed_within] ::= "shall" "be" "always" "performed" "within". {}
[in_the_case] ::= "in" "the" "case". {}
[formula] ::= [basic_formula] [shall_be_always_performed_within]
             [basic_term] [time_unit] [in_the_case] [basic_formula] "does" "not" "hold".

{G(infinity,
    (Implication((Negation (Formula_name $6)), (F(-3, (Formula_name $1))))))}
//If the gear is idle the gear is never N. N is a state.
```
// (gear == idle) -> G(Negation(gear == N))
[formula] ::= [if] "the" [basic_term] "is" [basic_term] "then" "it" "is" "never" [basic_term].
{Implication(
  (Eq((Term_name $3),(Term_name $5))),
  (G(infinity,(Neq((Term_name $3),(Term_name $10))))))}

// If the switch is not from/to gear N, a switch cannot be done in less than 400 ms.
[from_to] ::= "from". {}
[from_to] ::= "to". {}
[from_to] ::= "from/to". {}
[theswitchisnot] ::= "the" "switch" "is" "not". {}
[cannotbedoneinlessthan] ::= "cannot" "be" "done" "in" "less" "than". {}
[formula] ::= [if] [theswitchisnot] [from_to] "gear" [basic_term] "," "a" "switch"
[cannotbedoneinlessthan] [basic_term] [time_unit].
{Formula_name "AD_HOC_FORMULA"}

// The engine is guaranteed to find synchronous speed in the case where no error occurs in it.
//!ERROR -> F(infinity, SPEED==SYNCHRONOUS)
//if ERROR is false then ultimately SPEED is SYCHRONOUS.

[formula] ::= "if" [basic_formula] "is" "false" "then" "ultimately" [formula].
{Implication((Negation (Formula_name $2)), (F(infinity, (Formula_name $7)))))}
[formula] ::= "if" [basic_formula] "does" "not" "hold" "then" "ultimately" [formula].
{Implication((Negation (Formula_name $2)), (F(infinity, (Formula_name $8))))}

// The drift between the master clock and the slave clock is always bounded by the threshold D.
// The drift between MASTER_CLOCK and SLAVE_CLOCK is always bounded by D.
// G(infinity, Abs(MASTER_CLOCK-SLAVE_CLOCK) <= D)
// G(Leq(infinity, Abs(Minus((Term_name $4),(Term_name $6)), (Term_name $11))))
[the] ::= "the". {}
[the] ::= "The". {}
[drift] ::= "drift". {}
[drift] ::= "Drift". {}
[drift] ::= "absolute" "value" "of" "difference". {}
[drift] ::= "absolute" "difference". {}
[the_drift] ::= [the] [drift]. {}
[the_drift] ::= [drift]. {}

[drift-between] ::= [the_drift] "between" [term] "and" [term].
{Abs (Minus((Term_name $3),(Term_name $5)))}
[is_always_bounded_by] ::= "is" "never" "more" "than". {}
[is_always_bounded_by] ::= "is" "always" "bounded" "by". {}
[is_always_bounded_by] ::= "is" "always" "less" "than" "or" "equal". {}
[threshold_term] ::= "the" "threshold" [term].
{Term_name $3}
[threshold_term] ::= "threshold" [term].
{Term_name $2}
[threshold_term] ::= [term].
{Term_name $1}
[formula] ::= [drift-between] [is_always_bounded_by] [threshold_term].
{G(infinity, (Leq((Term_name $1),(Term_name $3))))}