spot/doc/org/tut12.org

Working with LTL formulas with finite semantics

• Shell version
• Python version
• C++ version
• Final notes

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 call_from_ltlf(f="(a U b) & Fc").

3. Convert the resulting formula into a Büchi automaton:

   

4. Remove the alive property, after marking as accepting all states with an outgoing edge labeled by !alive. (Note that since Spot does not actually support state-based acceptance, it needs to keep a false self-loop on any accepting state without a successor in order to mark it as accepting.)

   

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 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
properties: very-weak
--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.

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 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
properties: very-weak
--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.

C++ version

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
properties: very-weak
--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.

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 is no next step. In particular, X(0) is true iff there is 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: