Table of Contents

HOA Format Tool Support

The following tools implement support for the HOA format, either as output or as input.

For your convenience, we provide a live CD to play around with the tools.

jhoafparser and cpphoafparser libraries

jhoafparser and cpphoafparser are Java/C++-based parser libraries for the HOA format. The parsers include an abstraction layer (HOAConsumer) allowing applications to react to the different parts of the format, as well as command-line tools that can be used for validation of HOA automata.

jhoafparser and cpphoafparser is distributed under the GNU Lesser General Public License, version 2.1

ltl2dstar

Since version 0.5.2, ltl2dstar can convert LTL formulas into three kinds of automata that can be output in the HOA format:

Since version 0.5.3, ltl2dstar can also read non-deterministic Büchi
automata in HOA format, either from external LTL-to-Büchi translators or as the input automaton
for determinization.

ltl2dstar's source code is distributed under the GNU General Public License, version 2.

ltl3ba

Since version 1.1.0, ltl3ba can translate LTL formulas into three kinds of automata that can be output in the HOA format:

ltl3ba's source code is distributed under the GNU General Public License, version 2.

ltl3dra

Since version 0.2, ltl3dra can translate LTL formulas into three kinds of automata that can be output in the HOA format:

ltl3dra's source code is distributed under the GNU General Public License, version 2.

PRISM

PRISM uses omega automata for probabilistic verification of LTL (and similar logics) against probabilistic models such as Markov chains and Markov processes. Since version 4.3, it includes support for plugging in external LTL-to-automaton generation tools using the HOA format. PRISM incorporates jhoafparser for the purposes of importing the generated automata and now supports verification of a variety of acceptance conditions: arbitrary generic acceptance conditions for Markov chains and Rabin or generalized Rabin conditions for Markov decision processes.

PRISM's source code is distributed under the GNU General Public License, version 2.

Rabinizer

Rabinizer 3 can translate can translate LTL formulas into four kinds of automata that can be output in the HOA format:

The web page and source code of Rabinizer does not state any license.

Spot

Spot 1.99.1 has several tools that can output or input these automata, and that support the generic acceptance condition. In addition to ltl2tgba and dstar2tgba (that can output generalized Büchi automata in HOA), there are the following tools:

In these tools, HOA support is currently limited to non-alternating automata. The implemented C++ parser supports streaming of automata, where the input can mix the HOA format, the LBT format and never claims.

Spot's source code is distributed under the GNU General Public License, version 3.

Live CD

You can obtain an ISO image (740MB, SHASUM: a23c47374b5a2ae7e31f9c9cb2d6908384c7cf29), containing a Debian Live CD with various tools preinstalled for your convenience. You can run it in a virtual machine or burn it on a DVD and boot from it.

Running in a virtual machine

As virtual machine, we have tried QEMU and VirtualBox.

For VirtualBox, create a new virtual machine, attach the ISO image as a CD-drive and boot. For RAM, use at least 512MB, preferably 1GB.

With KVM/QEMU on a Linux system, you can start the Live CD with

kvm -cdrom hoaf-live.iso -boot d -m 1024 -net nic -net user

or

qemu-system-i386 -cdrom hoaf-live.iso -boot d -m 1024 -net nic -net user

depending on your installation, providing the virtual machine with 1GB of RAM. If you omit the -net parameters, the VM will not have a network connection, but everything else should work fine. For the latter command, if your kernel supports KVM and you have enabled hardware virtualization support in the BIOS, you can use --enable-kvm to get much better performance.

Using the Live CD

After the initial boot, press Enter to boot the live system. When the boot process is completed, you can login to the graphical desktop, with username hoaf and password hoaf.

On the desktop, you will find links to the HOA format specification, a terminal and a README file, suggesting example command-lines to try.

Note, that the keyboard layout is initially set to US. To change the keyboard layout to match the one on your computer, start the terminal and run

setxkbmap lang

where lang is your language code, e.g., de for German, fr for French, ...

Enjoy!