Execution and monitoring of HOA automata with HOAX
Logic in Computer Science
2025-12-04 v1 Formal Languages and Automata Theory
Abstract
We present a tool called Hoax for the execution of {\omega}-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.
Cite
@article{arxiv.2507.11126,
title = {Execution and monitoring of HOA automata with HOAX},
author = {Luca Di Stefano},
journal= {arXiv preprint arXiv:2507.11126},
year = {2025}
}
Comments
To appear in RV'25