LTL2BA4JOSGi LICENSE: The License is GPL, since LTL2BA4J and ltl2ba are GPL as well. LTL2BA4JOSGi is a Java 5 interface for the LTL to Büchi automaton conversion tool ltl2ba. It has been modified from LTL2BA4J to take advantage of the OSGi framework to improve the loading of the native code. This makes it suitable for use with any platform that provides an implementation of the OSGi framework, such as Eclipse (http://www.eclipse.org/) or Rodin (http://www.event-b.org/). This means it is not suitable for use from the command line. The origional LTL2BA4J is available from http://www.sable.mcgill.ca/~ebodde/rv/ltl2ba4j/. ltl2ba is a C library that provides an implementation of an LTL to BA algorithm based on the translation algorithm by Gastin and Oddoux, presented at the CAV Conference, held in 2001, Paris, France 2001. The source and precomplied libraries for ltl2ba are included. Usage: Use the static methods provided in rwth.i2.ltl2ba4j.LTL2BA4J in order to perform the conversion. You can either enter formulas as String or as objects (see package "formula"). The returned state machine can be customized by setting another graph factory (see package "model"). The classes concerning the Java Native Interface are all situated in the package "internal". You should normally not be required to do any changes here. LTL2BA4JOSGi comes with precompiled instances of ltl2ba for Windows, Linux, FreeBSD and OS X. To make it work on another OS, compile everything in c-src (you may use the Makefile) and update the Bundle-NativeCode header in the bundle manifest.