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.
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.
cpphoafparser is distributed under the GNU Lesser General Public License, version 2.1
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
ltl2dstar's source code is distributed under the GNU General Public License, version 2.
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.
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 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 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 1.99.1 has several tools that can output or input these automata, and that support the generic acceptance condition. In addition to
dstar2tgba (that can output generalized Büchi automata in HOA), there are the following tools:
randaut: generates random automata with any acceptance condition,
autfilt: reads automata (in the HOA format, the LBT's format or never claims), transform them, filter them, and output them (in the HOA format, the LBT's format, as never claims, or dot output for graphical display)
ltlcross: compares and checks LTL/PSL translators (can read HOA, LBT, never claims, or ltl2dstar's output)
ltldo: Wrap existing LTL to Büchi translator tools, providing them all the range of input and output Spot supports. For instance running
ltldo spin -f GFa -Hwill use spin to translate
<>aand convert the result to the HOA format.
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.
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.
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
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.
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
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
lang is your language code, e.g.,
de for German,
fr for French, ...