# Working with LTL formulas with finite semantics

## Table of Contents

The LTL operators used by Spot are defined over infinite words, and the various type of automata supported are all ω-automata, i.e., automata over infinite words.

However there is a trick we can use in case we want to use Spot to build a finite automaton that recognize some LTLf (i.e. LTL with finite semantics) property. The plan is as follows:

1. Have Spot read the input LTLf formula as if it was LTL.
2. Rewrite this formula in a way that embeds the semantics of LTLf in LTL. First, introduce a new atomic proposition `alive` that will be true initially, but that will eventually become false forever. Then adjust all original LTL operators so that they have to be satisfied during the `alive` part of the word. For instance the formula `(a U b) & Fc` would be transformed into `alive & (a U (alive & b)) & F(alive & c) & (alive U G!alive)`.
3. Convert the resulting formula into a Büchi automaton:

4. Remove the `alive` property, and, while we are at it, simplify the Büchi automaton:

5. Interpret the above automaton as finite automaton. (This part is out of scope for Spot.)

The above sequence of operations was described by De Giacomo & Vardi in their IJCAI'13 paper and by Dutta & Vardi in their Memocode'14 paper. However, beware that the LTLf to LTL rewriting suggested in theorem 1 of the IJCAI'13 paper has a typo (`t(φ₁ U φ₂)` should be equal to `t(φ₁) U t(φ₂ & alive)`) that is fixed in the Memocode'14 paper, but that second paper forgets to ensure that `alive` holds initially, as required in the first paper…

## Shell version

The first four steps of the above sequence of operations can be executed as follows. Transforming LTLf to LTL can be done using `ltlfilt`'s `--from-ltlf` option, translating the resulting formula into a Büchi automaton is obviously done with `ltl2tgba`, and removing an atomic proposition from an automaton can be done using `autfilt`'s `--remove-ap` option (adding `--small` will also simplify the automaton). Interpreting the resulting Büchi automaton as a finite automaton is out of scope for Spot.

```ltlfilt --from-ltlf -f "(a U b) & Fc" |
ltl2tgba -B |
autfilt --remove-ap=alive -B --small
```
```HOA: v1
States: 4
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0
[!2] 0
[2] 3
State: 1
[0&!2] 0
[!0&1&!2] 1
[!0&1&2] 2
[0&2] 3
State: 2
[!0&1] 2
[0] 3
State: 3 {0}
[t] 3
--END--
```

Use `-B -D` instead of `-B` if you want to ensure that a deterministic automaton is output.

## Python version

In Python, we use the `from_ltlf()` function to convert from LTLf to LTL and translate the result into a Büchi automaton using `translate()` as usual. Then we need to use the `remove_ap()` object, which we must first setup with some atomic propositions to remove. Finally we call the `postprocess()` function for automata simplifications. (Note that `postprocess()` is already called by `translate()`, but in this case removing the atomic proposition allows more simplification opportunities.)

```import spot
# Translate LTLf to Büchi.
aut = spot.from_ltlf('(a U b) & Fc').translate('ba')
# Remove "alive" atomic proposition
rem = spot.remove_ap()
rem.add_ap('alive')
aut = rem.strip(aut)
# Simplify result and print it.  Use postprocess('ba', 'det')
# if you always want a deterministic automaton.
aut = spot.postprocess(aut, 'ba')
print(aut.to_str('hoa'))
```
```HOA: v1
States: 4
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0
[!2] 0
[2] 3
State: 1
[0&!2] 0
[!0&1&!2] 1
[!0&1&2] 2
[0&2] 3
State: 2
[!0&1] 2
[0] 3
State: 3 {0}
[t] 3
--END--
```

If you need to print the automaton in a custom format (some finite automaton format probably), you should check our example of custom print of an automaton.

## C++ version

The C++ version is straightforward adaptation of the Python version. The Python functions `translate()` and `postprocess()` are convenient wrappers around the `spot::translator` and `spot::postprocessor` objects that we need to use here.

```#include <iostream>
#include <spot/tl/parse.hh>
#include <spot/tl/ltlf.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/remprop.hh>

int main()
{
spot::parsed_formula pf = spot::parse_infix_psl("(a U b) & Fc");
if (pf.format_errors(std::cerr))
return 1;

spot::translator trans;
trans.set_type(spot::postprocessor::BA);
trans.set_pref(spot::postprocessor::Small);
spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f));

spot::remove_ap rem;
rem.add_ap("alive");
aut = rem.strip(aut);

spot::postprocessor post;
post.set_type(spot::postprocessor::BA);
post.set_pref(spot::postprocessor::Small); // or ::Deterministic
aut = post.run(aut);

print_hoa(std::cout, aut) << '\n';
return 0;
}
```
```HOA: v1
States: 4
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: terminal
--BODY--
State: 0
[!2] 0
[2] 3
State: 1
[0&!2] 0
[!0&1&!2] 1
[!0&1&2] 2
[0&2] 3
State: 2
[!0&1] 2
[0] 3
State: 3 {0}
[t] 3
--END--
```

Again, please check our example of custom print of an automaton if you need to print in some format for NFA/DFA.

## Final notes

Spot only deals with infinite behaviors, so if you plan to use Spot to perform some LTLf model checking, you should stop at step 3. Keep the `alive` proposition in your property automaton, and also add it to the Kripke structure representing your system.

Alternatively, if your Kripke structure is already equipped with some `dead` property (as introduced by default in our `ltsmin` interface), you could replace `alive` by `!dead` by using ```ltlfilt --from-ltl="!dead"``` (from the command-line), a running `from_ltlf(f, "!dead")` in Python or C++.

When working with LTLf, there are two different semantics for the next operator:

• The weak next: `X a` is true if `a` hold in the next step or if there are no next step. In particular, `X(0)` is true iff there are no successor. (By the way, you cannot write `X0` because that as an atomic proposition: use `X(0)` or `X 0`.)
• The strong next: `X[!] a` is true if `a` hold in the next step and there must be a next step. In particular `X[!]1` asserts that there is a successor.