Working with LTL formulas with finite semantics

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 while adapting the accepting states can be done with autfilt's --to-finite option. 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 --to-finite

HOA: v1
States: 4
Start: 2
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!2] 0
[2] 1
State: 1 {0}
[t] 1
State: 2
[0&!2] 0
[0&2] 1
[!0&1&!2] 2
[!0&1&2] 3
State: 3
[0] 1
[!0&1] 3
--END--

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

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 call the to_finite() function.

import spot
# Translate LTLf to Büchi.
f = spot.from_ltlf('(a U b) & Fc')
aut = f.translate('small', 'buchi', 'sbacc')
# Remove "alive" atomic propositions and print result.
print(spot.to_finite(aut).to_str('hoa'))

HOA: v1
States: 4
Start: 2
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!2] 0
[2] 1
State: 1 {0}
[t] 1
State: 2
[0&!2] 0
[0&2] 1
[!0&1&!2] 2
[!0&1&2] 3
State: 3
[0] 1
[!0&1] 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.

The C++ version is straightforward adaptation of the Python version. (The Python function translate() is a convenient Python-only wrappers around the spot::translator object 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::Buchi);
  trans.set_pref(spot::postprocessor::SBAcc
                 | spot::postprocessor::Small);
  spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f));
  aut = spot::to_finite(aut);
  print_hoa(std::cout, aut) << '\n';
  return 0;
}

HOA: v1
States: 4
Start: 2
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!2] 0
[2] 1
State: 1 {0}
[t] 1
State: 2
[0&!2] 0
[0&2] 1
[!0&1&!2] 2
[!0&1&2] 3
State: 3
[0] 1
[!0&1] 3
--END--

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

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 is 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.

To see the difference between X and X[!], consider the following translation of (a & Xa) | (b & X[!]b):

Note that because in reality Spot supports only transitions-based acceptance, and the above automaton is really stored as a Büchi automaton that we decide to interpret as a finite automaton, there is a bit of trickery involved to represent an "accepting state" without any successor. While such a state makes sense in finite automata, it makes no sense in ω-automata: we fake it by adding a self-loop labeled by false (internally, this extra edge is carrying the acceptance mark that is displayed on the state). For instance: