diff --git a/spot/bin/man/autfilt.x b/spot/bin/man/autfilt.x index d67e450ba..f5f572981 100644 --- a/spot/bin/man/autfilt.x +++ b/spot/bin/man/autfilt.x @@ -23,7 +23,22 @@ Proceedings of SPIN'15. LNCS 9232. That paper gives the motivation for options \fB\-\-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] .BR spot-x (7) .BR dstar2tgba (1) diff --git a/spot/bin/man/dstar2tgba.x b/spot/bin/man/dstar2tgba.x index 8caa0596d..bb0b2e384 100644 --- a/spot/bin/man/dstar2tgba.x +++ b/spot/bin/man/dstar2tgba.x @@ -94,6 +94,14 @@ LNCS 8461. Explains the SAT-based minimization techniques that can be used (on 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] .BR spot-x (7), .BR autfilt (1) diff --git a/spot/bin/man/ltlfilt.x b/spot/bin/man/ltlfilt.x index 7ef700249..ed234d45e 100644 --- a/spot/bin/man/ltlfilt.x +++ b/spot/bin/man/ltlfilt.x @@ -20,6 +20,13 @@ stutter-invariant LTL. Information Processing Letters 75(6): 261-263 Describes the transformation behind the \fB\-\-remove\-x\fR option. .TP \(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 Powerset Construction for Restricted Classes of ω-Automata. Proceedings of ATVA'07. LNCS 4762.