My paper “Execution and monitoring of HOA automata with HOAX” has been accepted to RV 2025 (tool track).

Abstract:

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.

The tool is open-source and can be found at https://github.com/lou1306/hoax. I am now planning to publish it on the Python package index to simplify the install process.