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:
- Have Spot read the input LTLf formula as if it was LTL.
- 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 thealive
part of the word. For instance the formula(a U b) & Fc
would be transformed intoalive & (a U (alive & b)) & F(alive & c) & (alive U G!alive)
. Convert the resulting formula into a Büchi automaton:
Remove the
alive
property, and, while we are at it, simplify the Büchi automaton:- 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('small', 'buchi', 'sbacc') # 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::Buchi); trans.set_pref(spot::postprocessor::SBAcc | 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::Buchi); post.set_pref(spot::postprocessor::SBAcc | 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 ifa
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 writeX0
because that as an atomic proposition: useX(0)
orX 0
.) - The strong next:
X[!] a
is true ifa
hold in the next step and there must be a next step. In particularX[!]1
asserts that there is a successor.