SATbased Minimization of Deterministic ωAutomata
Table of Contents
This page explains how to use ltl2tgba
, dstar2tgba
, or autfilt
to minimize deterministic automata using a SAT solver.
Let us first state a few facts about this minimization procedure.
 The procedure works only on deterministic Büchi automata: any recurrence property can be converted into a deterministic Büchi automaton, and sometimes there are several ways of doing so.
 Spot actually implements two SATbased minimization procedures: one
that builds a deterministic transitionbased Büchi automaton
(DTBA), and one that builds a deterministic transitionbased
ωautomaton with arbitrary acceptance condition (DTωA). In
ltl2tgba
anddstar2tgba
, the latter procedure is restricted to TGBA. Inautfilt
it can use different and acceptance conditions for input and output, so you could for instance input a Rabin automaton, and produce a Streett automaton.  These two procedures can optionally constrain their output to use statebased acceptance. (They simply restrict all the outgoing transitions of a state to belong to the same acceptance sets.)
 Spot is built using PicoSAT 965. This solver was chosen for its performances, simplicity of integration and license compatibility. However, it is still possible to use an external SAT solver (as described below).
ltl2tgba
anddstar2tgba
will always try to output an automaton. If they fail to determinize the property, they will simply output a nondeterministic automaton, if they managed to obtain a deterministic automaton but failed to minimize it (e.g., the requested number of states in the final automaton is too low), they will return that "unminimized" deterministic automaton. There are only two cases where these tool will abort without returning an automaton: when the number of clauses output by Spot (and to be fed to the SAT solver) exceeds \(2^{31}\), or when the SATsolver was killed by a signal.autfilt satminimize
will only output an automaton if the SATbased minimization was successful. Our FORTE'14 paper describes the SAT encoding for the minimization of deterministic BA and TGBA. Our LPAR'15 paper describes the generalization of the SAT encoding to deal with deterministic TωA with any acceptance condition.
How to change the SAT solver used
By default Spot uses PicoSAT 965), this SATsolver is built into the Spot library, so that no temporary files are used to store the problem.
The environment variable SPOT_SATSOLVER
can be used to change the
SAT solver used by Spot. This variable should describe a shell command
to run the SATsolver on an input file called %I
so that a model satisfying
the formula will be written in %O
. For instance to use Glucose 3.0, instead
of the builtin version of PicoSAT, define
export SPOT_SATSOLVER='glucose verb=0 model %I >%O'
We assume the SAT solver follows the input/output conventions of the SAT competition
Enabling SATbased minimization in ltl2tgba
or dstar2tgba
Both tools follow the same interface, because they use the same
postprocessing steps internally (i.e., the spot::postprocessor
class).
First, option D
should be used to declare that you are looking for
more determinism. This will tweak the translation algorithm used by
ltl2tgba
to improve determinism, and will also instruct the
postprocessing routine used by both tools to prefer a
deterministic automaton over a smaller equivalent nondeterministic
automaton.
However D
is not a guarantee to obtain a deterministic automaton,
even if one exists. For instance, D
fails to produce a
deterministic automaton for GF(a <> XXb)
. Instead we get a 9state
nondeterministic automaton.
ltl2tgba D 'GF(a <> XXb)' stats='states=%s, det=%d'
states=9, det=0
Option x tbadet
enables an additional
determinization procedure, that would otherwise not be used by D
alone. This procedure will work on any automaton that can be
represented by a DTBA; if the automaton to process use multiple
acceptance conditions, it will be degeneralized first.
On our example, x tbadet
successfully produces a deterministic
TBA, but a nonminimal one:
ltl2tgba D x tbadet 'GF(a <> XXb)' stats='states=%s, det=%d'
states=7, det=1
Option x satminimize
will turnon SATbased minimization. It also
implies x tbadet
, so there is no need to supply both options.
ltl2tgba D x satminimize 'GF(a <> XXb)' stats='states=%s, det=%d'
states=4, det=1
We can draw it:
ltl2tgba D x satminimize 'GF(a <> XXb)' d
Clearly this automaton benefits from the transitionbased
acceptance. If we want a traditional Büchi automaton, with
statebased acceptance, we only need to add the B
option. The
result will of course be slightly bigger.
ltl2tgba BD x satminimize 'GF(a <> XXb)' d
There are cases where ltl2tgba
's tbadet
algorithm fails to produce a deterministic automaton.
In that case, SATbased minimization is simply skipped. For instance:
ltl2tgba D x satminimize 'G(F(!b & (X!a M (F!a & F!b))) U !b)' stats='states=%s, det=%d'
states=5, det=0
The question, of course, is whether there exist a deterministic
automaton for this formula, in other words: is this a recurrence
property? There are two ways to answer this question using Spot and
some help from ltl2dstar
.
The first is purely syntactic. If a formula belongs to the class of
"syntactic recurrence formulas", it expresses a syntactic property.
(Of course there are formulas that expresses a syntactic properties
without being syntactic recurrences.) ltlfilt
can be instructed to
print only formulas that are syntactic recurrences:
ltlfilt syntacticrecurrence f 'G(F(!b & (X!a M (F!a & F!b))) U !b)'
G(F(!b & (X!a M (F!a & F!b))) U !b)
Since our input formula was output, it expresses a recurrence property.
The second way to check whether a formula is a recurrence is by
converting a deterministic Rabin automaton using dstar2tgba
. The
output is guaranteed to be deterministic if and only if the input DRA
expresses a recurrence property.
ltlfilt removewm f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' l  ltl2dstar ltl2nba=spin:ltl2tgba@Ds    dstar2tgba D stats='input(states=%S) output(states=%s, accsets=%a, det=%d)'
input(states=11) output(states=9, accsets=1, det=1)
In the above command, ltldo
is used to convert the LTL formula into
ltl2dstar
's syntax. Then ltl2dstar
creates a deterministic Rabin
automaton (using ltl2tgba
as an LTL to BA translator), and the
resulting 11state DRA is converted
into a 9state DTBA by dstar2tgba
.
Since that result is deterministic, we can conclude that the formula
was a recurrence.
As far as SATbased minimization goes, dstar2tgba
will take the same
options as ltl2tgba
. For instance we can see that the smallest DTBA
has 4 states:
ltlfilt removewm f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' l  ltl2dstar ltl2nba=spin:ltl2tgba@Ds    dstar2tgba D x satminimize stats='input(states=%S) output(states=%s, accsets=%a, det=%d)'
input(states=11) output(states=4, accsets=1, det=1)
More acceptance sets
The formula "G(F(!b & (X!a M (F!a & F!b))) U !b)
" can in fact be minimized into an
even smaller automaton if we use multiple acceptance sets.
Unfortunately because dstar2tgba
does not know the formula being
translated, and it always convert a DRA into a DBA (with a single
acceptance set) before further processing, it does not know if using
more acceptance sets could be useful to further minimize it. This
number of acceptance sets can however be specified on the commandline
with option x satacc=M
. For instance:
ltlfilt removewm f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' l  ltl2dstar ltl2nba=spin:ltl2tgba@Ds    dstar2tgba D x satminimize,satacc=2 stats='input(states=%S) output(states=%s, accsets=%a, det=%d)'
input(states=11) output(states=3, accsets=2, det=1)
Beware that the size of the SAT problem is exponential in the number of acceptance sets (adding one acceptance set, in the input automaton or in the output automaton, will double the size of the problem).
The case of ltl2tgba
is slightly different because it can remember
the number of acceptance sets used by the translation algorithm, and
reuse that for SATminimization even if the automaton had to be
degeneralized in the meantime for the purpose of determinization.
Lowlevel details
The following figure (from our FORTE'14 paper) gives an overview of
the processing chains that can be used to turn an LTL formula into a
minimal DBA/DTBA/DTGBA. The blue area at the top describes ltl2tgba
D x satminimize
, while the purple area at the bottom corresponds
to dstar2tgba D x statminimize
.
The picture is slightly inaccurate in the sense that both ltl2tgba
and dstar2tgba
are actually using the same postprocessing chain:
only the initial translation to TGBA or conversion to DBA differs, the
rest is the same. However in the case of dstar2tgba
, no
degeneration or determinization are needed.
Also the picture does not show what happens when B
is used: any
DTBA is degeneralized into a DBA, before being sent to "DTBA SAT
minimization", with a special option to request statebased output.
The WDBAminimization boxes are able to produce minimal Weak DBA from
any TGBA representing an obligation property. In that case using
transitionbased or generalized acceptance will not allow further
reduction. This minimal WDBA is always used when D
is given
(otherwise, for the default small
option, the minimal WDBA is only
used if it is smaller than the nondeterministic automaton it has been
built from).
The "simplify" boxes are actually simulationbased reductions, and SCCbased simplifications.
The red boxes "not in TCONG" or "not a recurrence" correspond to situations where the tools will produce nondeterministic automata.
The following options can be used to finetune this procedure:

x tbadet
 attempt a powerset construction and check if there exists an acceptance set such that the resulting DTBA is equivalent to the input.

x satminimize
 enable SATbased minimization. It is the same as
x satminimize=1
(which is the default value). It performs a dichotomy to find the correct automaton size.This option impliesx tbadet
. 
x satminimize=[23]
 enable SATbased
minimization. Let us consider each intermediate automaton as a
step
towards the minimal automaton and assumeN
as the size of the starting automaton.2
and3
have been implemented with the aim of not restarting the encoding from scratch at each step. To do so, both restart the encoding afterN1(satincrsteps)
states have been won. Now, where is the difference? They both start by encoding the research of theN1
step and then:2
uses PicoSAT assumptions. It addssatincrsteps
assumptions (each of them removing one more state) and then checks direclty theN1(satincrsteps)
step. If such automaton is found, the process is restarted. Otherwise, a binary search begins betweenN1
andN1satincrsteps
. If not provided,satincrsteps
default value is 6.3
checks incrementally eachN(2+i)
step,i
ranging from0
tosatincrsteps
. This process is fully repeated until the minimal automaton is found. The last SAT problem solved correspond to the minimal automaton.satincrsteps
defaults to 2.
Both implies
x tbadet
. 
x satminimize=4
 enable SATbased minimization. It tries to reduce the
size of the automaton one state at a time. This option implies
x tbadet
. 
x satincrsteps=N
 set the value of
satincrsteps
to N. It doest not make sense to use it withoutx satminimize=2
orx satminimize=3
. 
x satacc=$m$
 attempt to build a minimal DTGBA with \(m\) acceptance sets.
This options implies
x satminimize
. 
x satstates=$n$
 attempt to build an equivalent DTGBA with \(n\)
states. This also implies
x satminimize
but won't perform any loop to lower the number of states. Note that \(n\) should be the number of states in a complete automaton, whileltl2tgba
anddstar2tgba
both remove sink states in their output by default (use optioncomplete
to output a complete automaton). Also note that even with thecomplete
option, the output automaton may have appear to have less states because the other are unreachable. 
x statebased
 for all outgoing transition of each state to belong to the same acceptance sets.

x !wdbaminimize
 disable WDBA minimization.
When options B
and x satminimize
are both used, x
statebased
and x satacc=1
are implied. Similarly, when option
S
and x satminimize
are both used, then option x statebased
is implied.
Using autfilt satminimize
to minimize any deterministic ωautomaton
This interface is new in Spot 1.99 and allows to minimize any deterministic ωautomaton, regardless of the acceptance condition used. By default, the procedure will try to use the same acceptance condition (or any inferior one) and produce transitionbased acceptance.
For our example, let us first generate a deterministic Rabin
automaton with ltl2dstar
.
ltlfilt f 'FGa  FGb' l 
ltl2dstar ltl2nba=spin:ltl2tgba@Ds outputformat=hoa   > output.hoa
Let's draw it:
autfilt output.hoa dot=.a
So this is a statebased Rabin automaton with two pairs. If we call
autfilt
with the satminimize
option, we can get the following
transitionbased version (the output may change depending on the SAT
solver used):
autfilt satminimize output.hoa dot=.a
We can also attempt to build a statebased version with
autfilt S satminimize output.hoa dot=.a
This is clearly smaller than the input automaton. In this example the acceptance condition did not change. The SATbased minimization only tries to minimize the number of states, but sometime the simplifications algorithms that are run before we attempt SATsolving will simplify the acceptance, because even removing a single acceptance set can halve the run time.
You can however force a specific acceptance to be used as output. Let's try with generalized coBüchi for instance:
autfilt S satminimize='acc="generalizedcoBuchi 2"' output.hoa dot=.a
Note that instead of naming the acceptance condition, you can actually give an acceptance formula in the HOA syntax. For example we can attempt to create a coBüchi automaton with
autfilt S satminimize='acc="Fin(0)"' output.hoa dot=.a
When forcing an acceptance condition, you should keep in mind that the
SATbased minimization algorithm will look for automata that have
fewer states than the original automaton (after preliminary
simplifications). This is not always reasonable. For instance
constructing a Streett automaton from a Rabin automaton might require
more states. An upper bound on the number of state can be passed
using a maxstates=123
argument to satminimize
.
If the input automaton is transitionbased, but option S
is used to
produce a statebased automaton, then the original automaton is
temporarily converted into an automaton with statebased acceptance to
obtain an upper bound on the number of states if you haven't specified
maxstate
. This upper bound might be larger than the one you would
specify by hand.
Here is an example demonstrating the case where the input automaton is smaller than the output. Let's take this small TGBA as input:
ltl2tgba 'GFa & GFb' >output2.hoa
autfilt output2.hoa dot=.a
If we attempt to minimize it into a transitionbased Büchi automaton, with fewer states, it will fail, output no result, and return with a nonzero exit code (because no automata where output).
autfilt satminimize='acc="Buchi"' output2.hoa echo $?
1
However if we allow more states, it will work:
autfilt satminimize='acc="Buchi",maxstates=3' output2.hoa dot=.a
By default, the SATbased minimization tries to find a smaller automaton by
performing a binary search starting from N/2
(N being the size of the
starting automaton). After various benchmarks, this algorithm proves to be the
best. However, in some cases, other rather similar methods might be better. The
algorithm to execute and some other parameters can be set thanks to the
satminimize
option.
The satminimize
option takes a comma separated list of arguments
that can be any of the following:

acc=DOUBLEQUOTEDSTRING
 where the
DOUBLEQUOTEDSTRING
is an acceptance formula in the HOA syntax, or a parametrized acceptance name (the differentaccname:
options from HOA). 
maxstates=N
 where
N
is an upperbound on the maximum number of states of the constructed automaton. 
states=M
 where
M
is a fixed number of states to use in the result (all the states needs not be accessible in the result, so the output might be smaller nonetheless). If this option is used the SATbased procedure is just used once to synthesize one automaton, and no further minimization is attempted. 
satincr=[12]
1
and2
correspond respectively tox satminimize=2
andx satminimize=3
options. They have been implemented with the aim of not restarting the encoding from scratch at each step  a step is a minimized intermediate automaton. To do so, both restart the encoding afterN1(satincrsteps)
states have been won N
being the size of the starting automaton. Now, where is the difference? They both start by encoding the research of theN1
step and then:1
uses PicoSAT assumptions. It addssteps
assumptions (each of them removing one more state) and then checks direclty theN1(satincrsteps)
step. If such automaton is found, the process is restarted. Otherwise, a binary search begins betweenN1
andN1satincrsteps
. If not provided,satincrsteps
defaults to 6.2
checks incrementally eachN(2+i)
step,i
ranging from0
tosatincrsteps
. This process is fully repeated until the minimal automaton is found. The last SAT problem solved correspond to the minimal automaton.satincrsteps
defaults to 2.
Both implies
x tbadet
.
satincrsteps=N
 set the value of
satincrsteps
toN
. This is used bysatincr
option. 
satnaive
 use the
naive
algorithm to find a smaller automaton. It starts fromN
and then checksN1
,N2
, etc. until the last successful check. 
satlangmap
 Find the lower bound of default satminimize procedure. This relies on the fact that the size of the minimal automaton is at least equal to the total number of different languages recognized by the automaton's states.

colored
 force all transitions (or all states if
S
is used) to belong to exactly one acceptance condition.
The colored
option is useful when used in conjunction with a parity
acceptance condition. Indeed, the parity acceptance condition by
itself does not require that the acceptance sets form a partition of
the automaton (which is expected from parity automata).
Compare the following, where parity acceptance is used, but the automaton is not colored:
autfilt S satminimize='acc="parity max even 3"' output2.hoa dot=.a
… to the following, where the automaton is colored, i.e., each state belong to exactly one acceptance set:
autfilt S satminimize='acc="parity max even 3",colored' output2.hoa dot=.a
Logging statistics
If the environment variable SPOT_SATLOG
is set to the name of a
file, the minimization function will append statistics about each of
its iterations in this file.
rm f stats.csv export SPOT_SATLOG=stats.csv ltlfilt f 'Ga R (F!b & (c U b))' l  ltl2dstar ltl2nba=spin:ltl2tgba@Ds    dstar2tgba D x satminimize,satacc=2 stats='input(states=%S) output(states=%s, accsets=%a, det=%d)' cat stats.csv
input(states=11) output(states=5, accsets=2, det=1) 5,,,,13600,1543042,81,2,141,0,"" 7,7,33,56,26656,4247441,207,11,570,0,"HOA: v1 States: 7 Start: 0 AP: 3 ""a"" ""b"" ""c"" accname: generalizedBuchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: translabels explicitlabels transacc complete deterministic BODY State: 0 [!0&1] 0 {0} [!0&!1&2] 0 {1} [!0&!1&!2] 1 {0} [0&!1&!2] 1 [0&!1&2] 2 {1} [0&1&2] 4 {0} [0&1&!2] 4 State: 1 [0&!1] 1 {0} [!0&!1&!2  0&1] 1 [!0&1  !0&2] 3 {0} State: 2 [!0&1] 0 {0 1} [!0&!1&2] 0 {1} [!0&!1&!2] 1 [0&!1&2] 2 [0&!1&!2] 3 {1} [0&1] 5 {0 1} State: 3 [!1&!2] 3 [1  2] 3 {0} State: 4 [!0&1] 0 {0} [!0&!1&2] 0 {0 1} [!0&!1&!2] 1 [0&1] 4 {0} [0&!1&2] 5 {0} [0&!1&!2] 6 State: 5 [!0&1  !0&2] 0 {0 1} [!0&!1&!2] 1 [0&1  0&2] 5 {0 1} [0&!1&!2] 6 {0} State: 6 [!0&!1&!2] 1 [!0&1&!2] 1 {0 1} [!0&1&2] 1 {1} [!0&!1&2] 3 {0 1} [0] 6 {0 1} END" 6,6,26,48,10512,1376507,70,0,218,0,"HOA: v1 States: 6 Start: 0 AP: 3 ""a"" ""b"" ""c"" accname: generalizedBuchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: translabels explicitlabels transacc complete deterministic BODY State: 0 [!0&1] 0 {0} [!0&!1&2] 0 {1} [!0&!1&!2] 1 [0&!1&!2] 1 {0 1} [0&!1&2] 2 {1} [0&1] 3 {0} State: 1 [t] 1 State: 2 [!0&1] 0 {0} [!0&!1&2] 0 {1} [!1&!2] 1 [0&!1&2] 2 {1} [0&1] 4 {1} State: 3 [!0&1] 0 [!0&!1&2] 0 {1} [!0&!1&!2] 1 [0&1] 3 [0&!1&2] 4 {1} [0&!1&!2] 5 {1} State: 4 [!0&1&2] 0 {0} [!0&!1&2  !0&1&!2] 0 {0 1} [!0&!1&!2] 1 [0&1  0&2] 4 {0 1} [0&!1&!2] 5 State: 5 [!0&!1&!2] 1 [!0&1  !0&2] 1 {0 1} [0] 5 {0 1} END"
The generated CSV file use the following columns:
 the n passed to the SATbased minimization algorithm (it means the input automaton had n+1 states)
 number of reachable states in the output of the minimization.
 number of edges in the output
 number of transitions
 number of variables in the SAT problem
 number of clauses in the SAT problem
 user time for encoding the SAT problem
 system time for encoding the SAT problem
 user time for solving the SAT problem
 system time for solving the SAT problem
 automaton produced
Times are measured with the times() function, and expressed in ticks (usually: 1/100 of seconds).
In the above example, the input DRA had 11
states. In the first line of the stats.csv
file, you can see the
minimization function searching for a 9 state DTBA and obtaining a
8state solution. (Since the minimization function searched for a
9state DTBA, it means it received a 10state complete DTBA, so the
processings performed before the minimization procedure managed to
convert the 11state DRA into a 10state DTBA.) Starting from the
8state solution, it looked for (and found) a 7state solution, and
then a 6state solution. The search for a 5state complete DTBA
failed. The final output is reported with 5 states, because by
default we output trim automata. If the complete
option had been
given, the useless sink state would have been kept and the output
automaton would have 6 states.