Ltl2ba

Jul 20, 2023

Fast translation from LTL formulae to Buchi automata

ltl2ba implements an algorithm of P. Gastin and D. Oddoux to generate Buchi automata from linear temporal logic LTL formulae. This algorithm generates a very weak alternating automaton and then transforms it into a Buchi automaton, using a generalized Buchi automaton as an intermediate step. Each automaton is simplified on-the-fly in order to save memory and time. As usual the LTL formula is simplified before any treatment. ltl2ba is more efficient than Spin 3.4.1, with regard to the size of the resulting automaton, the time of the computation, and the memory used.



Checkout these related ports:
  • Zn_poly - C library for polynomial arithmetic
  • Zimpl - Language to translate the LP models into .lp or .mps
  • Zegrapher - Software for plotting mathematical objects
  • Zarray - Dynamically typed N-D expression system based on xtensor
  • Z3 - Z3 Theorem Prover
  • Yices - SMT solver
  • Yacas - Yet Another Computer Algebra System
  • Xtensor - Multi-dimensional arrays with broadcasting and lazy computing
  • Xtensor-python - Python bindings for xtensor
  • Xtensor-io - Xtensor plugin to read/write images, audio files, numpy npz and HDF5
  • Xtensor-blas - BLAS extension to xtensor
  • Xspread - Spreadsheet program for X and terminals
  • Xppaut - Graphical tool for solving differential equations, etc
  • Xplot - X11 plotting package
  • Xlife++ - XLiFE++ eXtended Library of Finite Elements in C++