LTL2BA4J - Java bridge to ltl2ba

News

May 10th, 2005

The precompiled Win32 DLL had been compiled without support for the Next operator, which lead to syntax errors. An updated version is now available. Thanks to Dayou Zhou for pointing out this error.

Introduction

What is LTL2BA4J?

LTL2BA4J is a version of ltl2ba for Java, where ltl2ba is a tool written in ANSI C, which allows conversion of formulae in the Linear-time temporal logic LTL to Büchi automata.

Why would I use LTL2BA4J?

Well, if you don't know why, you probably wouldn't ;-)

There may be situations where you need Büchi automata which recoginze languages being recognized by an equivalent LTL formula, which you get as input.

What features does LTL2BA4J offer?

We offer the following powerful features:

• You may use LTL2BA4J as a commandline tool, which provides easy conversion of formulae in string format to automata in the dotty file format.
• Also you may use LTL2BA4J as a library:
  • We provide a factory mechanism that let's you construct formulae in a strongly typed way using Java objects.
• Retrieve the automaton and process it.

How does LTL2BA4J relate to jltl2ba?

jltl2ba is quite similar to our tool. However, it uses Runtime.exec(...) in order to invoke ltl2ba via the commandline and then parses its output in order to get back to an object structure. This is slow. We use the Java Native Interface (JNI) in order to access ltl2ba. This is much faster, since all the data conversion is directly handled in the virtual machine.

How does LTL2BA4J relate to Java Pathfinder?

As we found out, Java Pathfinder provides a LTL to Büchi automaton conversion engine as well. This is written in pure Java and provides the following two algorithms:

• Giannakopoulou, D. and Lerda, F. "From States to Transitions: Improving
  translation of LTL formulae to Buchi automata", FORTE 2002, LNCS 2529.
• Daniele, M., Giunchiglia, F., and Vardi, M.Y. "Improved Automata Generation
  for Linear Temporal Logic", CAV 1999, LNCS 1633.

Since it is pure Java, it may be slower. However, it's certainly easier to distribute.

Examples

Using strongly typed formulae

First you have to create a new FormulaFactory. This may either be the default implementation or a custom factory, you specify by your own.

IFormulaFactory factory = new FormulaFactory();

Then simply create the actual formula:

IFormula formula = factory.G(
                     factory.And(
                        factory.Proposition("prop1"),
                        factory.Not(
                                factory.Proposition("prop2")
                        )
                     )
                   );

formulae created that way are typesafe. They are guaranteed to always be parsed by ltl2ba (or it's a bug ;-) ).

Now create the automaton. formulaToBA will return a Collection of transitions.

for(ITransition t: formulaToBA(formula)) {
    System.out.println(t);
}

Using a custom graph factory

You can create custom graphs by just enabling a custom graph factory:

setGraphFactory(new MyGraphFactory());

Using a formula String

In oder to use a formula String, just use the overloaded version of formulaToBA:

for(ITransition t: formulaToBA("[] <> p")) {
    System.out.println(t);
}

In this case, of course you have to make sure that the input syntax is correct.

Download, Docs and License

Download

You may download LTL2BA4J here.

It comes with precompiled versions of ltl2ba for Win 32, Linux and FreeBSD. It also comes with full source, so you can compile ltl2ba yourself for your personal opertating system.

Documentation

Documentation can be found in the README file of the distribution as well as in the API docs here.

License

LTL2BA4J is available under the GPL license. It has to be, because ltl2ba is GPL as well.

Problems?

In case of any questions, please contact Eric Bodden or Volker Stolz.