Past-LTL to Future-LTL

One of the benchmarks used in our experimental evaluation is SynTech15, which consists of 17 specifications, 2 of them are inconsistent, so we only considered the same 15 specifications that the authors of the benchmark considered in the tool presented at  Maoz et.al.

Twelve of those specifications have Past-LTL operators, which are not supported by the tools used in our project. To deal with this problem, we manually translated all those specs to an equivalent version that only has pure future-LTL operators. We did this manually because automated translations from past-LTL to future-LTL can produce an exponential formula that is unsuitable for analysis.

As it is well known manual translations are error-prone so, we used NuSMV to check if our translations were equivalent to the originals or not.  After checking for realisability with Strix, we realized that 7 of the translated specifications were realizable. This is because the work of Maoz et.al., where SynTech15 was introduced, uses Spectra as a synthesis tool, while in our case, we use Strix. We analyze with NuSMV the equivalence between the semantics given by Spectra and Strix to the reactive specifications, and we find that they are not precisely equivalent. So, we ended up using just the remaining 5 specs. Below we present the translations we did to pass from Past-LTL to Future-LTL.

Let us briefly introduce the notion behind the translations.

Consider the following guarantee written in  Past-LTL: G ( Y(p) <-> q). For clarity, let's divide the biconditional into two implications, namely, G (Y(p) -> q && q -> Y(p)). We translated this formula as follows: G(p -> X(q) && X(q) -> p).

Despite this, the translations are still inconclusive because we have to include the initial states (this is due to the semantics of past-LTL operators). Remember the semantics of the past operator Yesterday(Y), it becomes false in the initial state.

Knowing that, the formula Y(p) -> q  in the initial states ends up being: false -> q, which is trivially true and the aforementioned guarantee partially holds.

On the other hand, the othe implication q -> Y(p) in the initial state is q -> false. If q holds in the initial state the system will never satisfy it so, we have to introduce the initial state !q.

Thus obtaining the final formula: (G(p -> X(q) && X(q) -> p)) && !q.

DOWNLOAD

You can download the file with all the translations and specifications from this link: SynTech15-future-LTL.

The file contains three folders: the original SynTech benchmark which contains all the spectra specifications; a folder containing the modified spectra files which include their corresponding translations and their initial states if necessary; a folder that contains all the tlsf files corresponding to each spectra specification.

Note: Each past-LTL formula that has been translated by us (i.e., those that were not included in the original spec) is marked by a text that indicates the beginning and end of each translation.