alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

doc: update bibliographic references

Browse source 
* doc/org/satmin.org, src/bin/man/dstar2tgba.x, src/bin/man/ltl2tgba.x:
Cite the FORTE'14 paper.
* doc/org/tools.org, src/bin/man/ltl2tgba.x: Replace the VECOS'11
citation by IJCCBS'14.
* src/bin/man/ltl2tgba.x: Cite SPIN'13.
This commit is contained in:
Alexandre Duret-Lutz 2014-05-14 18:16:12 +02:00
parent c46d6cee9a
commit 9761703736
4 changed files with 29 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
doc/org/satmin.org
View file

@ -31,8 +31,10 @@ Let us first state a few facts about this minimization procedure.
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.
6) Details about the SAT encoding used in the two procedures can be
found in our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]].
* How change the SAT solver used
* How to 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 -verb=0 -model %I

6
doc/org/tools.org
View file

@ -60,9 +60,9 @@ the following articles:
This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
- *LTL translation improvements in Spot*, /Alexandre Duret-Lutz/.
In Proc. of VECoS'11. Electronic Workshops in Computing. Tunis, Tunisia, Sep. 2011.
([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.11.vecos][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.slides.pdf][slides]])
- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/.
Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]])
This describes the translation from LTL to TGBA used by =ltl2tgba=
and =ltl2tgta=.

12
src/bin/man/dstar2tgba.x
View file

@ -2,7 +2,7 @@
dstar2tgba \- convert Rabin or Streett automata into Büchi automata
[BIBLIOGRAPHY]
.TP
1.
1.
<http://www.ltl2dstar.de/docs/ltl2dstar.html>
Documents the output format of ltl2dstar.
@ -28,5 +28,15 @@ dstar2tgba implements this for the Rabin case only. In other words,
translating a deterministic Rabin automaton with dstar2tgba will
produce a deterministic TGBA or BA if such a automaton exists.
.TP
4.
Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
of deterministic generalized Büchi automata. Proceedings of FORTE'14.
LNCS 8461.
Explains the SAT-based minimization techniques that can be used (on
request only) by dstar2tgba to minimize deterministic Büchi automata.
[SEE ALSO]
.BR spot-x (7)

13
src/bin/man/ltl2tgba.x
View file

@ -85,11 +85,22 @@ If you would like to give a reference to this tool in an article,
we suggest you cite one of the following papers:
.TP
\(bu
Alexandre Duret-Lutz: LTL translation improvements in Spot. Proceedings of VECoS'11.
Alexandre Duret-Lutz: LTL translation improvements in Spot 1.0.
Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
.TP
\(bu
Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
Proceedings of ATVA'13. LNCS 8172.
.TP
\(bu
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
and Jan Strejček: Compositional approach to suspension and other
improvements to LTL translation. Proceedings of SPIN'13. LNCS 7976.
.TP
\(bu
Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
of deterministic generalized Büchi automata. Proceedings of FORTE'14.
LNCS 8461.
[SEE ALSO]
.BR spot-x (7)