Page d'accueil du CNRS Page d'accueil de Paris Diderot Page d'accueil du LIAFA
LIAFA
Laboratoire d'Informatique Algorithmique: Fondements et Applications
CNRS UMR 7089, Université Paris Diderot - Paris 7, Case 7014
75205 Paris Cedex 13 - Tél: +33(0)1.57.27.92.56 - Fax: +33(0)1.57.27.94.09
Page d'accueil de la fondation Sciences Mathématiques de Paris Page d'accueil de FRMPC
   Annuaire      Contact      Accès au LIAFA      UFR d'informatique      Webmail   


English version

Rapports de recherche

  • Numéro du rapport: 2001-06
  • Auteurs: Paul Gastin and Denis Oddoux
  • Titre: Fast LTL to Büchi Automata Translation
  • Revised version of this technical report in the Proceedings of CAV`01, Lecture Notes in Computer Science 2102, p. 53-65, 2001.
  • Résumé:


     We present an algorithm to generate Büchi automata from LTL formulae. This algorithm generates a very weak alternating 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



  • Rapport complet:
    Format PostScript compressé avec gzip
    Format PostScript
    Format pdf

 
 ©  LIAFA 1995, dernière mise à jour: Mai 2013 webmestre[at]liafa.univ-paris-diderot.fr