1 [NAME] 2 ltlfilt \- filter files or lists of LTL/PSL formulas 3 [DESCRIPTION] 4 .\" Add any additional description here 5 [BIBLIOGRAPHY] 6 If you would like to give a reference to this tool in an article, 7 we suggest you cite the following paper: 8 .TP 9 \(bu 10 Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. 11 Proceedings of ATVA'13. LNCS 8172. 12 .PP 13 The following papers describe algorithms used by ltlfilt: 14 .TP 15 \(bu 16 Kousha Etessami: A note on a question of Peled and Wilke regarding 17 stutter-invariant LTL. Information Processing Letters 75(6): 261-263 18 (2000). 19 20 Describes the transformation behind the \fB\-\-remove\-x\fR option. 21 .TP 22 \(bu 23 Thibaud Michaud and Alexandre Duret-Lutz: 24 Practical stutter-invariance checks for ω-regular languages. 25 Proceedings of SPIN'15. LNCS 9232. 26 27 Describes the algorithm used by \fB\-\-stutter\-insensitive\fR option. 28 .TP 29 \(bu 30 Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the 31 Powerset Construction for Restricted Classes of 32 ω-Automata. Proceedings of ATVA'07. LNCS 4762. 33 34 Describes the checks implemented by the \fB\-\-safety\fR, 35 \fB\-\-guarantee\fR, and \fB\-\-obligation\fR options. 36 .TP 37 \(bu 38 Ivana Černá, Radek Pelánek: Relating Hierarchy of Temporal Properties 39 to Model Checking. Proceedings of MFCS'03. LNCS 2747. 40 41 Describes the syntactic LTL classes matched by the 42 \fB\-\-syntactic\-safety\fR, \fB\-\-syntactic\-guarantee\fR, 43 \fB\-\-syntactic\-obligation\fR options, 44 \fB\-\-syntactic\-persistence\fR, and \fB\-\-syntactic\-recurrence\fR 45 options. 46 .TP 47 \(bu 48 Kousha Etessami, Gerard J. Holzmann: Optimizing Büchi 49 Automata. Proceedings of CONCUR'00. LNCS 1877. 50 51 Describe the syntactic LTL classes matched by \fB\-\-eventual\fR, and 52 \fB\-\-universal\fR. 53 .TP 54 \(bu 55 Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and 56 Linear Dynamic Logic on Finite Traces. Proceedings of IJCAI'13. 57 58 Describe the transformation implemented by \fB\-\-from\-ltlf\fR 59 to reduce LTLf model checking to LTL model checking. 60 [SEE ALSO] 61 .BR randltl (1), 62 .BR ltldo (1) 63