1 [NAME] 2 genltl \- generate LTL formulas from scalable patterns 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 Prefixes used in pattern names refer to the following papers: 14 .TP 15 ccj 16 J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi 17 Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS'09. 18 .TP 19 dac 20 M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property 21 Specification Patterns for Finite-state Verification. 22 Proceedings of FMSP'98. 23 .TP 24 eh 25 K. Etessami and G. J. Holzmann: Optimizing Büchi Automata. 26 Proceedings of Concur'00. LNCS 1877. 27 .TP 28 gh 29 J. Geldenhuys and H. Hansen: Larger automata and less 30 work for LTL model checking. Proceedings of Spin'06. LNCS 3925. 31 .TP 32 hkrss 33 J. Holeček, T. Kratochvila, V. Řehák, D. Šafránek, and P. Šimeček: 34 Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004. 35 .TP 36 go 37 P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. 38 Proceedings of CAV'01. LNCS 2102. 39 .TP 40 kr 41 O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic 42 Automata. 43 Proceedings of MoChArt'10. LNAI 6572. 44 .TP 45 kv 46 O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. 47 ACM Transactions on Computational Logic, 6(2):273-294, 2005. 48 .TP 49 ms 50 D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata. 51 Proceedings of GandALF'17. EPTCS 256. 52 .TP 53 p 54 R. Pelánek: BEEM: benchmarks for explicit model checkers 55 Proceedings of Spin'07. LNCS 4595. 56 .TP 57 pps 58 N. Piterman, A. Pnueli, and Y. Sa'ar: Synthesis of Reactive(1) Designs. 59 Proceedings of VMCAI'06. LNCS 3855. 60 .TP 61 rv 62 K. Rozier and M. Vardi: LTL Satisfiability Checking. 63 Proceedings of Spin'07. LNCS 4595. 64 .TP 65 sb 66 F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. 67 Proceedings of CAV'00. LNCS 1855. 68 .TP 69 sejk 70 S. Sickert, J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic 71 Büchi Automata for Linear Temporal Logic. 72 Proceedings of CAV'16. LNCS 9780. 73 .TP 74 tv 75 D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. 76 Proceedings of RV'10. LNCS 6418. 77 78 [SEE ALSO] 79 .BR genaut (1), 80 .BR ltlfilt (1), 81 .BR randaut (1), 82 .BR randltl (1) 83