dstar2tgba

The following command instructs ltl2dstar to:

1. run ltl2tgba -Ds to build a Büchi automaton for (a U b) & GFb, and then
2. convert that Büchi automaton into a deterministic Rabin automaton (DRA) stored in fagfb.

Additionally, we use ltlfilt to convert our formula to the prefix format used by ltl2dstar.

ltlfilt -f '(a U b) & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - fagfb

By looking at the file fagfb you can see the ltl2dsar actually produced a 4-state DRA:

cat fagfb

DRA v2 explicit
Comment: "DBA2DRA[NBA=3]"
States: 4
Acceptance-Pairs: 1
Start: 1
AP: 2 "a" "b"
---
State: 0
Acc-Sig:
0
0
0
0
State: 1
Acc-Sig:
0
1
3
3
State: 2
Acc-Sig:
2
2
3
3
State: 3
Acc-Sig: +0
2
2
3
3

Let's display this automaton with autfilt:

autfilt fagfb --dot

dstar2tgba can now be used to convert this DRA into a TGBA, a BA, or a Monitor, using the same options as ltl2tgba.

For instance here is the conversion to a Büchi automaton (-B):

dstar2tgba -B fagfb -d

Note that by default the output is not complete. Use -C if you want a complete automaton.

But we could as well require the output as a never claim for Spin (option -s):

dstar2tgba -s fagfb

never {
T0_init:
  if
  :: ((a) && (!(b))) -> goto T0_init
  :: (b) -> goto accept_S2
  fi;
T0_S1:
  if
  :: (!(b)) -> goto T0_S1
  :: (b) -> goto accept_S2
  fi;
accept_S2:
  if
  :: (!(b)) -> goto T0_S1
  :: (b) -> goto accept_S2
  fi;
}

Here is the translation of GFa | GFb to a 4-state Streett automaton:

ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
autfilt --dot gfagfb

And now its conversion by dstar2tgba to a 1-state TGBA.

dstar2tgba gfagfb -d

The dstar2tgba tool implements a 4-step process:

1. read the automaton
2. convert it into TGBA
3. post-process the resulting TGBA (simplifying the automaton, degeneralizing it into a BA or Monitor if requested)
4. output the resulting automaton

BTW, the above scenario is also exactly what you get with autfilt if you run it as autfilt --tgba --high --small. (This is true only since version 1.99.4, since both tools can now read the same file formats.)

The last two steps are shared with ltl2tgba and use the same options.

The type of automaton to produce can be selected using the -B or -M switches:

-b, --buchi, --Buchi       automaton with Büchi acceptance
-B, --sba, --ba            state-based Büchi Automaton (same as -S -b)
    --cobuchi, --coBuchi   automaton with co-Büchi acceptance (will
                           recognize a superset of the input language if not
                           co-Büchi realizable)
-C, --complete             output a complete automaton
-G, --generic              any acceptance condition is allowed
-M, --monitor              Monitor (accepts all finite prefixes of the given
                           property)
-p, --colored-parity[=any|min|max|odd|even|min odd|min even|max odd|max
    even]                  colored automaton with parity acceptance
-P, --parity[=any|min|max|odd|even|min odd|min even|max odd|max even]
                           automaton with parity acceptance
-S, --state-based-acceptance, --sbacc
                           define the acceptance using states
    --tgba, --gba          automaton with Generalized Büchi acceptance
                           (default)

And these may be refined by a simplification goal, should the post-processor routine had a choice to make:

-a, --any                  no preference, do not bother making it small or
                           deterministic
-D, --deterministic        prefer deterministic automata (combine with
                           --generic to be sure to obtain a deterministic
                           automaton)
    --small                prefer small automata (default)

The effort put into post-processing can be limited with the --low or --medium options:

--high                 all available optimizations (slow, default)
--low                  minimal optimizations (fast)
--medium               moderate optimizations

For instance using -a --low will skip any optional post-processing, should you find dstar2tgba too slow.

Finally, the output format can be changed with the following common ouput options:

-8, --utf8                 enable UTF-8 characters in output (ignored with
                           --lbtt or --spin)
    --check[=PROP]         test for the additional property PROP and output
                           the result in the HOA format (implies -H).  PROP
                           may be some prefix of 'all' (default),
                           'unambiguous', 'stutter-invariant',
                           'stutter-sensitive-example', 'semi-determinism',
                           or 'strength'.
-d, --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|i(ID)|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#]                             
                           GraphViz's format.  Add letters for (1) force
                           numbered states, (a) show acceptance condition
                           (default), (A) hide acceptance condition, (b)
                           acceptance sets as bullets, (B) bullets except for
                           Büchi/co-Büchi automata, (c) force circular
                           nodes, (C) color nodes with COLOR, (d) show
                           origins when known, (e) force elliptic nodes, (E)
                           force rEctangular nodes, (f(FONT)) use FONT, (g)
                           hide edge labels, (h) horizontal layout, (i) or
                           (i(GRAPHID)) add IDs, (k) use state labels when
                           possible, (K) use transition labels (default), (n)
                           show name, (N) hide name, (o) ordered transitions,
                           (r) rainbow colors for acceptance sets, (R) color
                           acceptance sets by Inf/Fin, (s) with SCCs, (t)
                           force transition-based acceptance, (u) hide true
                           states, (v) vertical layout, (y) split universal
                           edges by color, (+INT) add INT to all set numbers,
                           (<INT) display at most INT states, (#) show
                           internal edge numbers
-H, --hoaf[=1.1|i|k|l|m|s|t|v]   Output the automaton in HOA format
                           (default).  Add letters to select (1.1) version
                           1.1 of the format, (b) create an alias basis if
                           >=2 AP are used, (i) use implicit labels for
                           complete deterministic automata, (s) prefer
                           state-based acceptance when possible [default],
                           (t) force transition-based acceptance, (m) mix
                           state and transition-based acceptance, (k) use
                           state labels when possible, (l) single-line
                           output, (v) verbose properties
    --lbtt[=t]             LBTT's format (add =t to force transition-based
                           acceptance even on Büchi automata)
    --name=FORMAT          set the name of the output automaton
-o, --output=FORMAT        send output to a file named FORMAT instead of
                           standard output.  The first automaton sent to a
                           file truncates it unless FORMAT starts with '>>'.
-q, --quiet                suppress all normal output
-s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                           select (6) Spin's 6.2.4 style, (c) comments on
                           states
    --stats=FORMAT, --format=FORMAT
                           output statistics about the automaton

The --stats options can output statistics about the input and the output automaton, so it can be useful to search for particular pattern.

For instance here is a complex command that will

1. generate an infinite stream of random LTL formulas with randltl,
2. use ltlfilt to rewrite the W and M operators away (--remove-wm), simplify the formulas (-r), remove duplicates (u) as well as formulas that have a size less than 3 (--size-min=3), and keep only the 10 first formulas (-n 10)
3. loop to process each of these formulas:
   • print it
   • then convert the formula into ltl2dstar's input format, process it with ltl2dstar (using ltl2tgba as the actual LTL->BA translator), and process the result with dstar2tgba to build a Büchi automaton (-B), favoring determinism if we can (-D), and finally displaying some statistics about this conversion.

The statistics displayed in this case are: %S, the number of states of the input (Rabin) automaton, %s, the number of states of the output (Büchi) automaton, %d, whether the output automaton is deterministic, and %p whether the automaton is complete.

randltl -n -1 --tree-size=10..14 a b c |
ltlfilt --remove-wm -r -u --size-min=3 -n 10 |
while read f; do
  echo "$f"
  ltlfilt -l -f "$f" |
  ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
  dstar2tgba -B --stats='  DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
done

(b | Fa) R Fc
  DRA: 9st.; BA: 6st.; det.? 1; complete? 1
Ga U G(!a | Gc)
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
GFc
  DRA: 2st.; BA: 2st.; det.? 1; complete? 1
!a | (a R b)
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
Xc R G(b | G!c)
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
c & G(b | F(a & c))
  DRA: 4st.; BA: 3st.; det.? 1; complete? 0
XXFc
  DRA: 4st.; BA: 4st.; det.? 1; complete? 1
XFc | Gb
  DRA: 4st.; BA: 4st.; det.? 1; complete? 1
G((a & F!c) U (!a | Ga))
  DRA: 6st.; BA: 3st.; det.? 1; complete? 1
a & !b
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0

An important point you should be aware of when comparing these numbers of states is that the deterministic automata produced by ltl2dstar are complete, while the automata produced by dstar2tgba (deterministic or not) are not complete by default. This can explain a difference of one state (the so-called "sink" state).

You can instruct dstar2tgba to output a complete automaton using the --complete option (or -C for short).

Spot implements several acceptance conversion algorithms. There is one generic cases, with some specialized variants.