From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata

  • Dimitra Giannakopoulou
  • Flavio Lerda
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


Model checking is an automated technique for checking that a system satisfies a set of required properties. With explicit-state model checkers, properties are typically defined in linear-time temporal logic (LTL), and are translated into Büchi automata in order to be checked. This paper describes how, by labeling automata transitions rather than states, we significantly reduce the size of automata generated by existing tableau-based translation algorithms. Our optimizations apply to the core of the translation process, where generalized Büchi automata are constructed. These automata are subsequently transformed in a single efficient step into Büchi automata as used by model checkers. The tool that implements the work described here is released as part of the Java Path- Finder software (JPF), an explicit state model checker of Java programs under development at the NASA Ames Research Center.


Model Check Current Node Linear Temporal Logic Propositional Variable Linear Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    Visser, W., Havelund, K., Brat, G., and Park, S. “Model Checking Programs”, in Proc. of the 15th IEEE International Conference on Automated Software Engineering (ASE’2000. 11–15 September 2000, Grenoble, France. IEEE Computer Society, pp. 3–11. Y. Ledru, P. Alexander, and P. Flener, Eds.Google Scholar
  2. [2]
    Holzmann, G.J., The Model Checker SPIN. IEEE Transactions on Software Engineering, Vol. 23(5), May 1997: pp. 279–295.CrossRefMathSciNetGoogle Scholar
  3. [3]
    Courcoubetis, C., Vardi, M., Wolper, P., and Yannakakis, M., Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design, Vol. 1, 1992: pp. 275–288.CrossRefGoogle Scholar
  4. [4]
    Etessami, K. and Holzmann, G. “Optimizing Buechi automata”, in Proc. of the 11th International Conference on Concurrency Theory (CONCUR’2000). August 2000, Pennsylvania, USA. Springer, LNCS 1877.Google Scholar
  5. [5]
    Somenzi, F. and Bloem, R. “Efficient Buechi automata from LTL Formulae”, in Proc. of the 12th International Conference on Computer Aided Verification (CAV 2000). July 2000, Chicago, USA. Springer, LNCS 1855. E.A. Emerson and A.P. Sistla, Eds.Google Scholar
  6. [6]
    Gerth, R., Peled, D., Vardi, M.Y., and Wolper, P. “Simple On-the-fly Automatic Verification of Linear Temporal Logic”, in Proc. of the 15th IFIP/WG6.1 Symposium on Protocol Specification, Testing and Verification (PSTV’95). June 1995, Warsaw, Poland.Google Scholar
  7. [7]
    Daniele, M., Giunchiglia, F., and Vardi, M.Y. “Improved Automata Generation for Linear Temporal Logic”, in Proc. of the 11th International Conference on Computer Aided Verification (CAV 1999). July 1999, Trento, Italy. Springer, LNCS 1633.Google Scholar
  8. [8]
    Gastin, P. and Oddoux, D. “Fast LTL to Buechi Automata Translation”, in Proc. of the 13th International Conference on Computer Aided Verification (CAV 2001). July 2001, Paris, France. Springer, LNCS 2102, pp. 53–65. G. Berry, H. Comon, and A. Finkel, Eds.Google Scholar
  9. [9]
    Clarke, E.M., Grumberg, O., and Peled, D.A., Model Checking: The MIT press, 1999.Google Scholar
  10. [10]
    Giannakopoulou, D. and Lerda, F., “Efficient translation of LTL formulae into Büchi automata”, RIACS, Technical Report, 01.29, June 2001.Google Scholar
  11. [11]
    Wolper, P. “Constructing Automata from Temporal Logic Formulas: A Tutorial”, in Proc. of the FMPA 2000 summer school. July 2000, Nijmegen, the Netherlands.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Dimitra Giannakopoulou
    • 1
  • Flavio Lerda
    • 2
  1. 1.RIACS/USRANASA Ames Research CenterMoffett FieldUSA
  2. 2.School of Computer Science, Carnegie Mellon UniversityPittsburghUSA

Personalised recommendations