Commit 3076c3da authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: document SAT-based minimization

* doc/org/, doc/org/satmin.tex: New files.
* doc/ Add them.
* doc/org/ Point to
* NEWS: Mention satmin.html.
parent cda847e2
......@@ -68,6 +68,8 @@ New in spot 1.1.4a (not relased)
deterministic automaton more efficiently) and is disabled by
default. See the spot-x(7) man page for documentation about the
related options: sat-minimize, sat-states, sat-acc, state-based.
See also for some
- ltlfilt, genltl, and randltl now have a --latex option to output
formulas in a way that its easier to embed in a LaTeX document.
......@@ -68,7 +68,15 @@ ORG_FILES = \
org/ \
org/ \
org/ \
org/ \
org/ \
org/satmin.tex \
$(srcdir)/org/satmin.png: org/satmin.tex
cd $(srcdir)/org && \
pdflatex -shell-escape satmin.tex && \
rm -f satmin.pdf satmin.aux satmin.log
$(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac)
make org && touch $@
#+TITLE: SAT-based Minimization of Deterministic (Generalized) Büchi Automata
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.html
This page explains how to use [[][=ltl2tgba=]] or [[][=dstar2tgba=]] to minimize
deterministic automata using a SAT solver.
Let us first state a few facts about this minimization procedure.
1) 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.
2) Spot actually implement two SAT-based minimization procedures: one
that builds a deterministic transition-based Büchi automaton
(DTBA), and one the builds a deterministic transition-based
generalized Büchi automaton (DTGBA). For the latter, we can supply
the number $m$ of acceptance sets to use.
3) These two procedures can optionally constrain their output to
use state-based acceptance. (They simply restrict all the outgoing
transitions of a state to belong to the same acceptance sets.)
4) A SAT solver should be installed for this to work. (Spot does not
distribute any SAT solver.)
5) [[][=ltl2tgba=]] and [[][=dstar2tgba=]] 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 SAT-solver was
killed by a signal.
* How change the SAT solver used
The environment variable =SPOT_SATSOLVER= can be used to change the
SAT solver used by Spot. The default is "=glucose %I >%O=", therefore
if you have installed [[][=glucose=]] in your =$PATH=, it should work right
away. Otherwise you may redefine this variable to point the correct
location or to another SAT solver. The =%I= and =%O= sequences will be
replaced by the names of temporary files containing the input for the
SAT solver and receiving its output. We assume that the SAT solver
should follow the conventions of the [[][SAT competition]] for input and
* Enabling SAT-based minimization for deterministic automata
Both tools follow the same interface, because they use the same
post-processing steps internally (i.e., the =spot::postprocessor=
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
post-processing routine used by both tools to prefer a
deterministic automaton over a smaller equivalent nondeterministic
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 9-state
non-deterministic automaton.
#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D "GF(a <-> XXb)" --stats='states=%s, det=%d'
: states=9, det=0
Option =-x tba-det= 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 tba-det= successfully produces a deterministic
TBA, but a non-minimal one:
#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D -x tba-det "GF(a <-> XXb)" --stats='states=%s, det=%d'
: states=7, det=1
Option =-x sat-minimize= will turn-on SAT-based minimization. It also
implies =-x tba-det=, so there is no need to supply both options.
#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" --stats='states=%s, det=%d'
: states=4, det=1
We can draw it:
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -D -x sat-minimize "GF(a <-> XXb)"
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1"]
1 -> 1 [label="a & !b\n"]
1 -> 2 [label="!b & !a\n"]
1 -> 2 [label="b & !a\n{Acc[1]}"]
1 -> 3 [label="a & b\n{Acc[1]}"]
2 [label="2"]
2 -> 4 [label="!b & !a\n"]
2 -> 4 [label="b & !a\n{Acc[1]}"]
2 -> 3 [label="a & !b\n"]
2 -> 3 [label="a & b\n{Acc[1]}"]
3 [label="4"]
3 -> 1 [label="a & !b\n{Acc[1]}"]
3 -> 1 [label="a & b\n"]
3 -> 2 [label="!b & !a\n{Acc[1]}"]
3 -> 2 [label="b & !a\n"]
4 [label="3"]
4 -> 2 [label="!b & !a\n{Acc[1]}"]
4 -> 4 [label="b & !a\n"]
4 -> 3 [label="a & !b\n{Acc[1]}"]
4 -> 3 [label="a & b\n"]
#+NAME: gfaexxb3
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/'
#+RESULTS: gfaexxb3
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1"]
1 -> 1 [label="a & !b\\n"]
1 -> 1 [label="a & b\\n{Acc[1]}"]
1 -> 2 [label="!b & !a\\n"]
1 -> 2 [label="b & !a\\n{Acc[1]}"]
2 [label="2"]
2 -> 3 [label="!b & !a\\n"]
2 -> 3 [label="b & !a\\n{Acc[1]}"]
2 -> 4 [label="a & !b\\n"]
2 -> 4 [label="a & b\\n{Acc[1]}"]
3 [label="3"]
3 -> 1 [label="a & !b\\n{Acc[1]}"]
3 -> 3 [label="b & !a\\n"]
3 -> 4 [label="!b & !a\\n{Acc[1]}"]
3 -> 4 [label="a & b\\n"]
4 [label="4"]
4 -> 1 [label="a & !b\\n{Acc[1]}"]
4 -> 1 [label="a & b\\n"]
4 -> 2 [label="!b & !a\\n{Acc[1]}"]
4 -> 2 [label="b & !a\\n"]
#+BEGIN_SRC dot :file gfaexxb3.png :cmdline -Tpng :var txt=gfaexxb3 :exports results
Clearly this is automaton benefit from the transition-based
acceptance. If we want a traditional Büchi automaton, with
state-based acceptance, we only need to add the =-B= option. The
result will of course be slightly bigger.
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)"
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1", peripheries=2]
1 -> 2 [label="!a\n{Acc[1]}"]
1 -> 3 [label="a & !b\n{Acc[1]}"]
1 -> 4 [label="a & b\n{Acc[1]}"]
2 [label="2", peripheries=2]
2 -> 1 [label="!b & !a\n{Acc[1]}"]
2 -> 4 [label="a\n{Acc[1]}"]
2 -> 5 [label="b & !a\n{Acc[1]}"]
3 [label="4"]
3 -> 1 [label="a & b\n"]
3 -> 2 [label="b & !a\n"]
3 -> 3 [label="a & !b\n"]
3 -> 6 [label="!b & !a\n"]
4 [label="3"]
4 -> 1 [label="!b\n"]
4 -> 3 [label="a & b\n"]
4 -> 6 [label="b & !a\n"]
5 [label="6"]
5 -> 1 [label="!b\n"]
5 -> 4 [label="a & b\n"]
5 -> 5 [label="b & !a\n"]
6 [label="5"]
6 -> 1 [label="a & b\n"]
6 -> 2 [label="b & !a\n"]
6 -> 4 [label="a & !b\n"]
6 -> 5 [label="!b & !a\n"]
#+NAME: gfaexxb4
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/'
#+RESULTS: gfaexxb4
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1", peripheries=2]
1 -> 1 [label="!b & !a\\n{Acc[1]}"]
1 -> 2 [label="b & !a\\n{Acc[1]}"]
1 -> 3 [label="a\\n{Acc[1]}"]
2 [label="2"]
2 -> 1 [label="!b & !a\\n"]
2 -> 2 [label="b & !a\\n"]
2 -> 3 [label="a & !b\\n"]
2 -> 4 [label="a & b\\n"]
3 [label="3", peripheries=2]
3 -> 5 [label="!a\\n{Acc[1]}"]
3 -> 6 [label="a\\n{Acc[1]}"]
4 [label="5"]
4 -> 1 [label="!b & !a\\n"]
4 -> 5 [label="b & !a\\n"]
4 -> 3 [label="a & !b\\n"]
4 -> 6 [label="a & b\\n"]
5 [label="4"]
5 -> 1 [label="b & !a\\n"]
5 -> 2 [label="!b & !a\\n"]
5 -> 3 [label="a & b\\n"]
5 -> 4 [label="a & !b\\n"]
6 [label="6"]
6 -> 1 [label="b & !a\\n"]
6 -> 5 [label="!b & !a\\n"]
6 -> 3 [label="a & b\\n"]
6 -> 6 [label="a & !b\\n"]
#+BEGIN_SRC dot :file gfaexxb4.png :cmdline -Tpng :var txt=gfaexxb4 :exports results
There are cases where =ltl2tgba='s =tba-det= algorithm fails to produce a deterministic automaton.
In that case, SAT-based minimization is simply skipped. For instance:
#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d'
: states=4, 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:
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --syntactic-recurrence -f "Ga R (F!b & (c U b))"
: Ga R (F!b & (c 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.
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f "Ga R (F!b & (c U b))" -l |
ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - |
dstar2tgba -D --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
: input(states=11) output(states=9, acc-sets=1, det=1)
In the above command, =ltlfilt= 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 11-state DRA is converted into a 9-state DTBA by
=dstar2tgba=. Since that result is deterministic, we can conclude
that the formula was a recurrence.
As far as SAT-based minimization goes, =dstar2tgba= will take the same
options as =ltl2tgba=, so we for instance check that the smallest DTBA
has 6 states:
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f "Ga R (F!b & (c U b))" -l |
ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - |
dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
: input(states=11) output(states=6, acc-sets=1, det=1)
* More acceptance sets
The formula "=Ga R (F!b & (c 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 command-line
with option =-x sat-acc=M=. For instance:
#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f "Ga R (F!b & (c U b))" -l |
ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - |
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
: input(states=11) output(states=5, acc-sets=2, det=1)
Beware that the size of the SAT problem is exponential in the number of acceptance sets.
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 SAT-minimization even if the automaton had to be
degeneralized in the meantime for the purpose of determinization.
* Low-level details
The following figure 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 sat-minimize=, while
the purple area at the bottom corresponds to =dstar2tgba -D -x
The picture is slightly inaccurate in the sense that both =ltl2tgba=
and =dstar2tgba= are actually using the same post-processing 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 state-based output.
The WDBA-minimization boxes are able to produce minimal Weak DBA from
any TGBA representing an obligation property. In that case using
transition-based 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 simulation-based reductions, and
SCC-based simplifications.
The red boxes "not in TCONG" or "not a recurrence" correspond to
situations where the tools will produce non-deterministic automata.
The following options can be used to fine-tune this procedure:
- =-x tba-det= :: attempt a powerset construction and check if
there exists a acceptance set such that the
resulting DTBA is equivalent to the input
- =-x sat-minimize= :: enable SAT-based minimization. By default it
tries to reduce the size of the automaton one state at a time.
This option implies =-x tba-det=.
- =-x sat-minimize=2= :: enabled SAT-based minimization, but perform a
dichotomy to locate the correct automaton size. Use this only if
you suspect that the optimal size is far away from the input
size. This option implies =-x tba-det=.
- =-x sat-acc=$m$= :: attempt to build a minimal DTGBA with $m$ acceptance sets.
This options implies =-x sat-minimize=.
- =-x sat-states=$n$= :: attempt to build an equivalent DTGBA with $n$
states. This also implies =-x sat-minimize= 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, while =ltl2tgba=
and =dstar2tgba= both remove sink states in their output by
default (use option =--complete=) to output a complete automaton.
Also note that even with the =--complete= option, the output
automaton may have appear to have less states because the other
are unreachable.
- =-x state-based= :: for all outgoing transition of each state
to belong to the same acceptance sets.
- =-x !wdba-minimize= :: disable WDBA minimization.
When options =-B= and =-x sat-minimize= both used, =-x state-based= and
=-x sat-acc=1= are implied.
\newcommand{\pin}[1]{\tikz[baseline=0]\node[fill=yellow,draw,circle,thin,inner sep=0.5pt,above left] {\footnotesize #1};}
\tikzstyle{dstep}=[align=center,minimum height=3em]
\tikzstyle{pstep}=[draw,dstep,drop shadow,fill=white]
\tikzstyle{iostep}=[dstep,rounded corners=1mm]
\begin{tikzpicture}[shorten >=1pt,>=stealth',semithick,node distance=5.5mm]
%\tikzset{callout/.style={ellipse callout, callout pointer arc=30,
% callout absolute pointer={#1},fill=blue!30,draw}}
\node[pstep] (trans) {translate\\to TGBA};
\node[pstep,right=of trans.0,xshift=-2mm] (wdba) {attempt\\WDBA\\minim.};
\draw[->] (trans) -- (wdba);
\node[pstep,right=of wdba.0] (simp) {simplify\\TGBA};
\draw[->] (wdba) -- node[above]{fail} (simp);
\node[instep,below=of trans,yshift=-2mm] (ltl1) {LTL\\formula};
\draw[->] (ltl1) -- (trans);
\node[pstep,right=of simp,yshift=8mm,xshift=1mm] (degen) {degen\\to TBA};
\draw[->] (simp) -- ($(simp.east)+(2mm,0mm)$) |- node[above left,align=right,at end]{nondet. or\\$|\CF|>m=1$} (degen);
\coordinate[pstep,right=of degen,yshift=-8mm,xshift=-1mm] (isdet);
%\coordinate[pstep,right=of degen,yshift=-2em] (isdet2);
\draw[->] (simp) -- ($(simp.east)+(2mm,0mm)$) -- node[below right,at start]{else} (isdet);
\coordinate (degen2) at ($(degen.east)+(2mm,0mm)$);
\draw[->] (degen) -- (degen2) -- ($(simp.east -| degen2)$);
\node[pstep,right=of degen,xshift=2.5em] (tbadet) {attempt\\ powerset\\to DTBA};
\draw[->] (isdet) |- node[at end,above left]{nondet.} (tbadet);
\coordinate (tbadet2) at ($(tbadet.east)+(2mm,0mm)$);
\node[errstep,right=of tbadet.0,xshift=2mm,yshift=2mm] (nottcong) {not in\\$\mathsf{TCONG}$};
\draw[->] (tbadet) -- node[at end,above left,align=center]{fail} ($(nottcong.180 |- tbadet)$);
\coordinate (turn) at ($(nottcong.-130 |- simp.0)$);
\draw[->] (isdet) -- node[below right,at start]{det.} (turn);
\draw[->] (tbadet2) -- node[right,pos=.6]{success} ($(tbadet2 |- turn)$);
\node[pstep,below=of tbadet.-125,yshift=-3mm] (dtbasat) {DTBA SAT\\minimization};
\node[pstep,below=of dtbasat,yshift=5mm] (dtgbasat) {DTGBA SAT\\minimization};
\draw[->] (turn) |- node[above left]{$m=1$} (dtbasat);
\draw[->] (turn) |- node[above left]{$m>1$} (dtgbasat);
\node[outstep,left=of dtgbasat] (mindtgba) {minimal\\DTGBA};
\node[outstep] at ($(mindtgba |- dtbasat)$) (mindtba) {minimal\\DTBA};
\node[outstep,left=of mindtba,xshift=5mm] (wdbaok) {minimal\\WDBA};
\draw[->] (wdba) |- coordinate(c1) node[above right]{success} (wdbaok);
\draw[->] (dtgbasat) -- (mindtgba);
\draw[->] (dtbasat) -- (mindtba);
\node[pstep,below=of ltl1,yshift=-2mm,xshift=1mm] (ltl2dstar) {\texttt{ltl2dstar}\\(DRA)};
\draw[->] (ltl1) -- ($(ltl1 |- ltl2dstar.90)$);
\node[pstep,right=of ltl2dstar] (dra2dba) {attempt\\conversion\\to DBA};
\draw[->] (ltl2dstar) -- (dra2dba);
\node[pstep,right=of dra2dba,xshift=3em] (wdba2) {attempt\\WDBA\\minim.};
\node[pstep,right=of wdba2,xshift=2em] (simp2) {simplify as\\DBA or DTBA};
\draw[->] (dra2dba) -- node[at start,below right]{success} (wdba2);
\draw[->] (wdba2) -- node[at start,below right]{fail} (simp2);
\coordinate (turn2) at ($(turn |- simp2)$);
\draw[->] (simp2) -- (turn2);
\draw[] (turn2) -- (turn);
\node[errstep] (notrec) at ($(ltl1 -| dra2dba)$) {not a\\ recurrence};
\draw[->] (dra2dba) -- node[right]{fail} (notrec);
\draw[->] (wdba2.160) -| node[below right,sloped]{success} (wdbaok);
\begin{scope}[on background layer]
\coordinate (pt1) at ($(tbadet.north east)+(3mm,2mm)$);
\coordinate (pt2) at ($(mindtba.north east)+(3mm,0mm)$);
\coordinate (pt3) at ($(mindtgba.south east)+(0mm,-1mm)$);
\coordinate[xshift=1mm,yshift=1mm] (turn3) at (turn);
\path[pattern color=blue!30,pattern=north west lines] ($(trans.west |- pt1)$) |- (pt2) |- (pt3) -| (turn3) -| (pt1) -- cycle;
\node[below right] at ($(trans.west |- pt1)$) {\texttt{ltl2tgba}};
\coordinate[yshift=1mm,xshift=1mm] (pt4) at ($(pt2 -| turn3)$);
\coordinate[yshift=-3mm,xshift=-1mm] (pt5) at ($(dra2dba.south west)$);
\coordinate[yshift=1mm,xshift=-1mm] (pt6) at ($(dra2dba.north west)$);
\path[pattern color=blue!30!red!30,pattern=north east lines] (pt5) -| (pt4) -- ($(pt2) + (1mm,1mm)$) |- (pt6) -- cycle;
\node[above left,yshift=-1mm] at ($(pt5 -| pt4)$) {\texttt{dstar2tgba}};
%\node[fill=yellow,draw,ellipse callout,thin,inner sep=0.5pt,callout pointer arc=30,,yshift=6mm,callout absolute pointer={(c1)}] at (c1) {\footnotesize 1};
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
......@@ -44,6 +44,10 @@ corresponding commands are hidden.
- [[][=dstar2tgba=]] Convert deterministic Rabin or Streett automata into
Büchi automata.
* Advanced uses
- [[][SAT-based minimization of Deterministic (Generalized) Büchi automata]]
# LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl
# LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval
# LocalWords: setenv concat getenv setq
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment