# Execution and monitoring of HOA automata with HOAX

arXiv: https://arxiv.org/abs/2507.11126 · HTML: https://mlsanity.com/paper/2507.11126/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Jul 2025.

## Built on by (most cited first, 1 of 1)

- [Warm Starting State-Space Models with Automata Learning](https://mlsanity.com/paper/2603.05694/) (2026)

## Abstract (arXiv)

We present a tool called Hoax for the execution of ω-automata expressed in the popular HOA format. The tool leverages the notion of trap sets to enable runtime monitoring of any (non-parity) acceptance condition supported by the format. When the automaton is not monitorable, the tool may still be able to recognise so-called ugly prefixes, and determine that no further observation will ever lead to a conclusive verdict. The tool is open-source and highly configurable. We present its formal foundations, its design, and compare it against the trace analyser PyContract on a lock acquisition scenario.