Execution and monitoring of HOA automata with HOAX
Luca Di Stefano
TL;DR
The paper tackles the lack of execution tools for HOA ω-automata by introducing Hoax, a configurable, open-source engine that executes HOA automata and provides runtime monitoring via trap sets for non-parity acceptance conditions. It builds on formal notions of trap sets and BSCCs to enable a one-step monitor and verdicts (good/bad/ugly) or ⊥, including composition rules for complex acceptance conditions. The authors present a practical implementation with drivers and hooks, and validate it against PyContract on a lock-acquisition benchmark, highlighting performance trade-offs and interoperability with existing HOA tooling. The work demonstrates the feasibility and usefulness of trap-set based monitoring in HOA execution and outlines future directions to handle nondeterminism and richer logics to improve scalability and applicability.
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.