Trustworthy Intelligent Systems

Java Automata Learning Framework

On this page one can download our prototype tool jalf (Java Automata Learning Framework).

We provide it as a JAR file, so that it can be directly used on different platform without having to compile it. Note that this is still a development version, and may thus crash or produce unrefined error messages if used incorrectly. We recommend you to run jalf on a Linux machine and have Java 8 installed. Previous versions of Java have not been tested.

Brief usage instructions

jalf can be started using java -jar jalf.jar, which is equal to the following command

java -jar jalf.jar help

There are three running modes in jalf, namely test mode, interactive mode and automatic mode:

  1. test mode with -t n k. With this mode, you can test any algorithm integrated in the tool with n randomly generated Büchi automata of k states.
  2. interactive mode with -int. In this mode, you can teach the tool by yourself, which has not been tested.
  3. automatic mode with -aut. With this mode, we by default learn a finite automaton with the DK package answering all membership and equivalence queries, and we can also learn a Büchi automaton with the help of the RABIT tool.

The command to run jalf in automatic mode to learn the Büchi automaton given by aut.ba is:

java -jar jalf.jar aut.ba -aut -table -periodic -under

In *jalf, you can specify the data structures for the learning procedure in the following.

  1. -table. This argument calls for the use of the observation table.
  2. -tree. It requires to use the classification tree for the learner.

You can also use three canonical FDFAs to learn the Büchi automata as follows.

  1. -periodic. Learning the periodic FDFA.
  2. -syntactic. Learning the syntactic FDFA.
  3. -recurrent. Learning the recurrent FDFA.

If you want to learn the Büchi automaton using L~$~ automaton, you should use -ldollar instead of above arguments.

java -jar jalf.jar aut.ba -aut -table -ldollar

Moreover, you can also specify the method to transform an FDFA to a Büchi automaton. There are two methods.

  1. -under. This method under approximates the language of any given FDFA.
  2. -over. It over approximates the language of given FDFA.

You can also get a limit deterministic Büchi automaton if you use -ldba along with -under like

java -jar jalf.jar aut.ba -aut -table -periodic -under -ldba

Automata Input Format

jalf accepts an automaton in the BA format defined on the webpage of RABIT tool. Currently, we have added the support for converting an automaton in the HOAF format to the BA format by relating every propositional formula in HOAF file with a fresh symbol.

In order to reproduce the experimental results we obtained in the paper, please use the Büchi automata from Büchi Store.

Download jalf