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

man: more bibliographic references

Browse source 
* spot/bin/man/autfilt.x, spot/bin/man/dstar2tgba.x,
spot/bin/man/ltlfilt.x: Add more bibliography.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-07 22:23:10 +01:00
parent b519c7d3dc
commit 0edb2ad066
3 changed files with 30 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

15
spot/bin/man/autfilt.x
View file

@ -23,7 +23,22 @@ Proceedings of SPIN'15. LNCS 9232.
That paper gives the motivation for options \fB\-\-exclusive\-ap\fR That paper gives the motivation for options \fB\-\-exclusive\-ap\fR
and \fB\-\-simplify\-exclusive\-ap\fR. and \fB\-\-simplify\-exclusive\-ap\fR.
.TP
\(bu
Thibaud Michaud and Alexandre Duret-Lutz:
Practical stutter-invariance checks for ω-regular languages.
Proceedings of SPIN'15. LNCS 9232.
Describes the algorithms used by the \fB\-\-destut\fR and
\fB\-\-instut\fR options. These options correpond respectively to
cl() and sl() in the paper.
.TP
\(bu
Souheib Baarir and Alexandre Duret-Lutz: SAT-based minimization of
deterministic ω-automata. Proceedings of LPAR'15 (a.k.a LPAR-20).
LNCS 9450.
Describes the \fB\-\-sat\-minimize\fR option.
[SEE ALSO] [SEE ALSO]
.BR spot-x (7) .BR spot-x (7)
.BR dstar2tgba (1) .BR dstar2tgba (1)

8
spot/bin/man/dstar2tgba.x
View file

@ -94,6 +94,14 @@ LNCS 8461.
Explains the SAT-based minimization techniques that can be used (on Explains the SAT-based minimization techniques that can be used (on
request only) by dstar2tgba to minimize deterministic Büchi automata. request only) by dstar2tgba to minimize deterministic Büchi automata.
.TP
5.
Souheib Baarir and Alexandre Duret-Lutz: SAT-based minimization of
deterministic ω-automata. Proceedings of LPAR'15 (a.k.a LPAR-20).
LNCS 9450.
Extends the previous paper by allowing arbitrary acceptance
conditions.
[SEE ALSO] [SEE ALSO]
.BR spot-x (7), .BR spot-x (7),
.BR autfilt (1) .BR autfilt (1)

7
spot/bin/man/ltlfilt.x
View file

@ -20,6 +20,13 @@ stutter-invariant LTL. Information Processing Letters 75(6): 261-263
Describes the transformation behind the \fB\-\-remove\-x\fR option. Describes the transformation behind the \fB\-\-remove\-x\fR option.
.TP .TP
\(bu \(bu
Thibaud Michaud and Alexandre Duret-Lutz:
Practical stutter-invariance checks for ω-regular languages.
Proceedings of SPIN'15. LNCS 9232.
Describes the algorithm used by \fB\-\-stutter\-insensitive\fR option.
.TP
\(bu
Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the
Powerset Construction for Restricted Classes of Powerset Construction for Restricted Classes of
ω-Automata. Proceedings of ATVA'07. LNCS 4762. ω-Automata. Proceedings of ATVA'07. LNCS 4762.