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

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.

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.

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.