1 [NAME] 2 dstar2tgba \- convert automata into Büchi automata 3 [HISTORY] 4 .B dstar2tgba 5 was introduced in Spot 1.2 as a command that reads automata 6 in 7 .BR ltl2dstar 's 8 format, and converts them into TGBA. At this time it was 9 the only command-line tool being able to read automata. 10 .PP 11 In Spot 1.99.1 the 12 .B autfilt 13 command was introduced, but could only read automata 14 in the HOA format, or in 15 .BR lbtt 's 16 format, or as never claims. So 17 .B dstar2tgba 18 was still the only way to process automata 19 in 20 .BR ltl2dstar 's 21 format. 22 .PP 23 In Spot 1.99.4 the parser for 24 .BR ltl2dstar 's 25 format was finally merged with the parser 26 used by 27 .B autfilt 28 for reading the other format. This implies not only 29 that 30 .B autfilt 31 can now read 32 .BR ltl2dstar's 33 format, but also that 34 .B dstar2tgba 35 can read the other formats as well. 36 37 Nowadays, the command 38 .PP 39 .in +4n 40 .nf 41 .ft C 42 % dstar2tgba some files 43 .fi 44 .PP 45 can be used as a shorthand for 46 .PP 47 .in +4n 48 .nf 49 .ft C 50 % autfilt \-\-tgba \-\-high \-\-small some files 51 .fi 52 .PP 53 The name 54 .B dstar2tgba 55 is kept for backward compatibility and because it is used 56 in at least one published paper, but naming this tool 57 .B aut2tgba 58 would make more sense. 59 60 [BIBLIOGRAPHY] 61 .TP 62 1. 63 .UR http://www.ltl2dstar.de/docs/ltl2dstar.html 64 The 65 .BR ltl2dstar manual 66 .UE . 67 68 Documents the output format of 69 .BR ltl2dstar . 70 71 .TP 72 2. 73 Chistof Löding: Mehods for the Transformation of ω-Automata: 74 Complexity and Connection to Second Order Logic. Diploma Thesis. 75 University of Kiel. 1998. 76 77 Describes various tranformations from non-deterministic Rabin and 78 Streett automata to Büchi automata. Slightly optimized variants of 79 these transformations are used by dstar2tgba for the general cases. 80 81 .TP 82 3. 83 Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton: Deterministic 84 ω-automata vis-a-vis Deterministic Büchi Automata. ISAAC'94. 85 86 Explains how to preserve the determinism of Rabin and Streett automata 87 when the property can be repreted by a Deterministic automaton. 88 dstar2tgba implements this for the Rabin case only. In other words, 89 translating a deterministic Rabin automaton with dstar2tgba will 90 produce a deterministic TGBA or BA if such a automaton exists. 91 92 .TP 93 4. 94 Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization 95 of deterministic generalized Büchi automata. Proceedings of FORTE'14. 96 LNCS 8461. 97 98 Explains the SAT-based minimization techniques that can be used (on 99 request only) by dstar2tgba to minimize deterministic Büchi automata. 100 101 .TP 102 5. 103 Souheib Baarir and Alexandre Duret-Lutz: SAT-based minimization of 104 deterministic ω-automata. Proceedings of LPAR'15 (a.k.a LPAR-20). 105 LNCS 9450. 106 107 Extends the previous paper by allowing arbitrary acceptance 108 conditions. 109 [SEE ALSO] 110 .BR spot-x (7), 111 .BR autfilt (1) 112