LTL2BA swMATH ID: 10956 Software Authors: Gastin, Paul; Oddoux, Denis Description: Fast LTL to Büchi automata translation. We present an algorithm to generate Büchi automata from Linear Time Logic (LTL) formulae. This algorithm generates a very weak alternating co-Büchi automaton and then transforms it into a Büchi automaton, using a generalized Büchi automaton as an intermediate step. Each automaton is simplified on-the-fly in order to save memory and time. As usual we simplify the LTL formula before any treatment. We implemented this algorithm and compared it with Spin: the experiments show that our algorithm is much more efficient than Spin. The criteria of comparison are the size of the resulting automaton, the time of the computation and the memory used. Our implementation is available on the web at the following address: http://verif.liafa.jussieu.fr/ltl2ba. Homepage: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ Related Software: SPIN; SPOT; NuSMV; CESAR; lbtt; CUDD; PRISM; BEEM; Uppaal; Rabinizer; ltl2dstar; Isabelle/HOL; MONA; BLAST; VIS; Cadence SMV; Java PathFinder; GOAL; FoCs; Maude Cited in: 93 Publications all top 5 Cited by 195 Authors 5 Chen, Yu-Fang 4 Tsay, Yih-Kuen 3 Doyen, Laurent 3 Esparza, Javier 3 Geldenhuys, Jaco 3 Křetínský, Jan 3 Kupferman, Orna 3 Latvala, Timo 3 Meseguer Guaita, José 3 Raskin, Jean-François 3 Schneider, Klaus 3 Strejček, Jan 3 Tsai, Ming-Hsien 3 Vardi, Moshe Ya’akov 2 Abdulla, Parosh Aziz 2 Baier, Christel 2 Belta, Calin A. 2 Blahoudek, František 2 Chan, Wen-Chin 2 Chang, Jinn-Shu 2 Duan, Zhenhua 2 Duret-Lutz, Alexandre 2 Ehlers, Rüdiger 2 Eker, Steven 2 Fritz, Carsten 2 Gaiser, Andreas 2 Gastin, Paul 2 Heljanko, Keijo 2 Holík, Lukáš 2 Klein, Joachim 2 Kloetzer, Marius 2 Luo, Chi-Jian 2 Oddoux, Denis 2 Penczek, Wojciech 2 Qin, Zheng 2 Shan, Laixiang 2 Sridharanarayanan, Ambarish 2 Unel, Gulay 2 Valmari, Antti 2 Vojnar, Tomáš 2 Zbrzezny, Andrzej 1 Ábrahám, Erika 1 Baader, Franz 1 Babiak, Tomáš 1 Bae, Kyungmin 1 Barnat, Jiří 1 Bartha, Tamás 1 Basin, David A. 1 Becker, Bernd 1 Beneš, Nikola 1 Beyene, Tewodros A. 1 Bezděk, Peter 1 Bianculli, Domenico 1 Biere, Armin 1 Bloem, Roderick 1 Bonnet, Remi 1 Bradfield, Julian Charles 1 Castillos, Kalou Cabrera 1 Černá, Ivana 1 Chang, Yi-Wen 1 Chatterjee, Krishnendu 1 Chaudhuri, Swarat 1 Chen, Mingshi 1 Clarke, Edmund Melson jun. 1 Clemente, Lorenzo 1 Cofer, Darren D. 1 Cook, Byron 1 Couvreur, Jean-Michel 1 Cristau, Julien 1 Dadeau, Frédéric 1 Dajani-Brown, Samar 1 d’Amorim, Marcelo 1 Darvas, Dániel 1 de Moura, Leonardo 1 De Wulf, Martin 1 Dimitrova, Rayna 1 Ding, Xuchu 1 D’Souza, Deepak 1 Du, Xiaomin 1 Farzan, Azadeh 1 Faymonville, Peter 1 Finkbeiner, Bernd 1 Garavel, Hubert 1 Garis, Ana G. 1 George, Chris W. 1 Gutierrez, Julian 1 Hagihara, Shigeki 1 Hansen, Henri 1 Hao, Yujie 1 Hartmann, Gary L. 1 He, Jifeng 1 Hutschenreiter, Lisa 1 Jansen, Nils 1 Jantsch, Simon 1 Jobstmann, Barbara 1 Jones, Kevin D. 1 Julliand, Jacques 1 Junttila, Tommi A. 1 Kabanza, Froduald 1 Kanso, Bilal ...and 95 more Authors all top 5 Cited in 18 Serials 8 Theoretical Computer Science 5 Formal Methods in System Design 4 Formal Aspects of Computing 4 Logical Methods in Computer Science 3 Fundamenta Informaticae 3 Journal of Logical and Algebraic Methods in Programming 1 Acta Informatica 1 Artificial Intelligence 1 International Journal of Theoretical Physics 1 Automatica 1 Information and Computation 1 Discrete Event Dynamic Systems 1 Journal of Applied Mathematics 1 Journal of Applied Logic 1 Frontiers of Computer Science 1 Computer Science Review 1 Lecture Notes in Business Information Processing 1 Monographs in Theoretical Computer Science. An EATCS Series all top 5 Cited in 9 Fields 91 Computer science (68-XX) 43 Mathematical logic and foundations (03-XX) 4 Systems theory; control (93-XX) 3 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Operations research, mathematical programming (90-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Probability theory and stochastic processes (60-XX) 1 Quantum theory (81-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year