diff --git a/src/bin/man/ltlfilt.x b/src/bin/man/ltlfilt.x index cb5287bea..440e1397c 100644 --- a/src/bin/man/ltlfilt.x +++ b/src/bin/man/ltlfilt.x @@ -2,5 +2,38 @@ ltlfilt \- filter files or lists of LTL/PSL formulas [DESCRIPTION] .\" Add any additional description here +[BIBLIOGRAPHY] +.TP +1. +Kousha Etessami: A note on a question of Peled and Wilke regarding +stutter-invariant LTL. Information Processing Letters 75(6): 261-263 +(2000). + +Describes the transformation behind the \fB\-\-remove\-x\fR option. +.TP +2. +Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the +Powerset Construction for Restricted Classes of +ω-Automata. Proceedings of ATVA'07. LNCS 4762. + +Describes the checks implemented by the \fB\-\-safety\fR, +\fB\-\-guarantee\fR, and \fB\-\-obligation\fR options. +.TP +3. +Ivana Černá, Radek Pelánek: Relating Hierarchy of Temporal Properties +to Model Checking. Proceedings of MFCS'03. LNCS 2747. + +Describes the syntactic LTL classes matched by the +\fB\-\-syntactic\-safety\fR, \fB\-\-syntactic\-guarantee\fR, +\fB\-\-syntactic\-obligation\fR options, +\fB\-\-syntactic\-persistence\fR, and \fB\-\-syntactic\-recurrence\fR +options. +.TP +4. +Kousha Etessami, Gerard J. Holzmann: Optimizing Büchi +Automata. Proceedings of CONCUR'00. LNCS 1877. + +Describe the syntactic LTL classes matched by \fB\-\-eventual\fR, and +\fB\-\-universal\fR. [SEE ALSO] .BR randltl (1)