This graph represents a chronology of algorithms for translating LTL to Büchi automata. Three kinds of automata are distinguished:

Legend

Büchi automata with labeled and accepting states

Büchi automata with labeled transitions and accepting states

Büchi automata with labeled and accepting transitions (see TGBA)

All of them are as expressive as the other. It's easy to show that pink automata (i.e. TGBA) are more compact than blue automata which in turn are more compact that yellow automata. Some of the translation algorithms colored in pink actually use TGBA only as an intermediate step; it doesn't matter (since Spot handles TGBA we are interested by algorithms that produces TGBA at any moment).

Semantic Tableau\nBeth, 1959 Analytic Tableau\nSmullyan, 1968 Temporal Logic Can Be More Expressive\nWolper, 1983 Reasoning about infinite computation paths\nWolper et al., 1983 Reasoning about infinite computations\nVardi & Wolper, 1994 Tableau Method for TL\nWolper, 1985 Simple On-The-Fly Verification of LTL\nGerth et al., 1995 Alternating Finite Automata on w-words\nMiyano & Hayashi, 1984 Constructing BA from LTL using\nSimulation Relations for Alternating BA\nFritz, 2003 Checking that Finite State Concurrent Programs\nSatify their Linear Specification\nLichtenstein & Pnueli, 1985 Fair SMG and Linear Time Model Checking\nBarringer et al., 1989 Decision Algorithm for Full PTL\nKesten et al., 1993 Point de Vue Symbolique sur LTL\nCouvreur, 2000 On-The-Fly Verification of LTL\nCouvreur, 1999 Symbolic Model Checking:\n10^20 States and Beyond\nBurch et al., 1990 Improved Automata Generation for LTL\nDaniele et al., 1999 Optimizing Büchi Automata\nEtessami & Holzmann, 2000 Simple and Efficient Translation from LTL,\nThirioux, 2002 Wring\nSomenzi & Bloem, 2000 From States to Transitions\nGiannakopoulou & Lerda, 2002 Fast LTL to Büchi Automata translation\nGastin & Oddoux, 2001 Fair Simulation Relations, Parity Games,\n and State Space Reduction for BA\nEtessami et al., 2001 On translating LTL into\nAlternating and Nondeterministic Automata\nTauriainen, 2003 Automata and LTL: translations with transition-based acceptance\nHeikki Tauriainen, 2006

LtlTranslationAlgorithms/Genealogy (last edited 2007-03-24 15:49:33 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.