Fast LTL to Büchi Automata Translation

By Paul Gastin, Denis Oddoux. International Conference on Computer Aided Verification, 2001

767 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Runtime Verification for LTL and TLTL (2011, methodology): “…a monitor generator, in the following referred to as the LTL3 tools, which is available online under a public license.3 It relies on version 1.1 of LTL2BA, which is Gastin s and Oddoux s translator for converting LTL formulae into corresponding B ¨ uchi automata [Gastin and Oddoux 2001].”
The Maude 2.0 System (2003, methodology): “Rather than the classical tableaux construction [17], we use a newer technique proposed in [16] based on very weak alternating automata to which we add some strongly connected component optimizations adapted from those in [23].”
Temporal Logics for Hyperproperties (2013, methodology): “A model-checking algorithm for HyperLTL2 can developed from previously known algorithms for LTL model checking [29, 30, 71, 72].”
A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications (2008, methodology): “This is in essence a model checking problem, and we use standard tools based on Büchi automata [17].”
Model checking lots of systems: efficient verification of temporal properties in software product lines (2010, methodology): “The tool interfaces with ltl2ba,(5) based on [19], to automate the translation from LTL to BA, and uses Graphviz(6) to render FTS graphically.”
A Software Analysis Perspective (2012, methodology): “In the former case, Aoräı uses ltl2ba [29] to obtain an equivalent Büchi automaton.”